NEWS

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

New in spot 2.8.7 (2020-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.

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 such
    'Fin(1) & Inf(2) & Fin(0)' as 'Fin(0) | Fin(1) & Inf(2)'
    due to a bug in the is_generalized_rabin() matching function.

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.

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.

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

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.

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.

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 family.
    (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 persistence 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 has learned another trick to better
    merge states from transient 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 object 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 transient 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 longer 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 in-place 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.

New in spot 2.7.5 (2019-06-05)

  Build:

  - Although the Python bindings in this release are still done with
    Swig3.0, the code has been updated to be compatible with Swig4.0.

  Library:

  - print_dot will replace labels that have more 2048 characters by a
    "(label too long)" string.  This works around a limitation of
    GraphViz that aborts when some label exceeds 16k characters, and
    also helps making large automata more readable.

  Bugs fixed:

  - spot::translator was not applying Boolean sub-formula rewriting
    by default unless a spot::option_map was passed.  This caused some
    C++ code for translating certain formulas to be noticeably slower
    than the equivalent call to the ltl2tgba binary.

  - The remove_ap algorithm was preserving the "terminal property" of
    automata, but it is possible that a non-terminal input produces a
    terminal output after some propositions are removed.

New in spot 2.7.4 (2019-04-27)

  Bugs fixed:

  - separate_sets_here() (and therefore autfilt --separate-sets) could
    loop infinitely on some inputs.

  - In some situation, ltl2tgba -G could abort with
    "direct_simulation() requires separate Inf and Fin sets".  This
    was fixed by teaching simulation-based reductions how to deal
    with such cases.

  - The code for detecting syntactically stutter-invariant PSL
    formulas was incorrectly handling the ";" operator, causing some
    stutter-sensitive formulas to be flagged a stutter-invariant.

New in spot 2.7.3 (2019-04-19)

  Bugs fixed:

  - When processing CSV files with MSDOS-style \r\n line endings,
    --stats would output the \r as part of the %> sequence instead
    of ignoring it.

  - Fix serious typo in remove_alternation() causing incorrect
    output for some VWAA.  Bug introduced in Spot 2.6.

  Documentation:

  - Multiple typos and minor updates.

New in spot 2.7.2 (2019-03-17)

  Python:

  - Improved support for explicit Kripke structures.  It is now
    possible to iterate over a kripke_graph object in a way similar to
    twa_graph.

  Documentation:

  - A new page shows how to create explicit Kripke structures in C++
    and Python.  See https://spot.lrde.epita.fr/tut52.html
  - Another new page shows how to deal with LTLf formulas (i.e., LTL
    with finite semantics) and how to translate those.
    See https://spot.lrde.epita.fr/tut12.html

  Build:

  - Work around a spurious null dereference warning when compiling
    with --coverage and g++ 8.3.0-3 from Debian unstable.

New in spot 2.7.1 (2019-02-14)

  Build:

  - Work around GCC bug #89303 that causes memory leaks and std::weak_bad_ptr
    exceptions when Spot is compiled with the version of g++ 8.2 currently
    distributed by Debian unstable (starting with g++ 8.2.0-15).

  Python:

  - The following methods of spot::bdd_dict are now usable in Python when
    fine control over the lifetime of associations between BDD variables
    and atomic propositions is needed.
    - register_proposition(formula, for_me)
    - register_anonymous_variables(count, for_me)
    - register_all_propositions_of(other, for_me)
    - unregister_all_my_variables(for_me)
    - unregister_variable(var, for_me)

  - Better support for explicit Kripke structures:
    - the kripke_graph type now has Python bindings
    - spot.automaton() and spot.automata() now support a want_kripke=True
      to return a kripke_graph
      See the bottom of https://spot.lrde.epita.fr/ipynb/ltsmin-dve.html
      for some examples.

  Library:

  - Printing Kripke structures via print_hoa() will save state names.

  - kripke_graph_ptr objects now honor any "state-names" property
    when formatting states.

  Bugs fixed:

  - The print_dot_psl() function would incorrectly number all but the
    first children of commutative n-ary operators: in this case no
    numbering was expected.

  - std::out_of_range C++ exceptions raised from Python code are now
    converted into IndexError Python exceptions (instead of aborting
    the program).

  - The LTL parser would choke on carriage returns when command-line
    tools such as ltlfilt, ltlcross, or ltl2tgba were run on files of
    formulas with MS-DOS line endings.

  - The core translation for unambiguous automata was incorrectly
    tagging some non-weak automata as weak.

  - The product_susp() function used to multiply an automaton with a
    suspendable automaton could incorrectly build transition-based
    automata when multiplying two state-based automata.  This caused
    ltl2tgba to emit error messages such as: "automaton has
    transition-based acceptance despite prop_state_acc()==true".

New in spot 2.7 (2018-12-11)

  Command-line tools:

  - ltlsynt now has three algorithms for synthesis:
    --algo=sd     is the historical one. The automaton of the formula
                  is split to separate inputs and outputs, then
                  determinized (with Safra construction).
    --algo=ds     the automaton of the formula is determinized (Safra),
                  then split to separate inputs and outputs.
    --algo=lar    translate the formula to a deterministic automaton
                  with an arbitrary acceptance condition, then turn it
                  into a parity automaton using LAR, and split it.
    In all three cases, the obtained parity game is solved using
    Zielonka algorithm. Calude's quasi-polynomial time algorithm has
    been dropped as it was not used.

  - ltlfilt learned --liveness to match formulas representing liveness
    properties.

  - the --stats= option of tools producing automata learned how to
    tell if an automaton uses universal branching (%u), or more
    precisely how many states (%[s]u) or edges (%[e]u) use universal
    branching.

  Python:

  - spot.translate() and spot.postprocess() now take an xargs=
    argument similar to the -x option of ltl2tgba and autfilt, making
    it easier to fine tune these operations.  For instance
        ltl2tgba 'GF(a <-> XXa)' --det -x gf-guarantee=0
    would be written in Python as
        spot.translate('GF(a <-> XXa)', 'det', xargs='gf-guarantee=0')
    (Note: those extra options are documented in the spot-x(7) man page.)

  - spot.is_generalized_rabin() and spot.is_generalized_streett() now return
    a tuple (b, v) where b is a Boolean, and v is the vector of the sizes
    of each generalized pair.  This is a backward incompatible change.

  Library:

  - The LTL parser learned syntactic sugar for nested ranges of X
    using the X[n], F[n:m], and G[n:m] syntax of TSLF.  (These
    correspond to the next!, next_e!, and next_a! operators of PSL,
    but we do not support those under these names currently.)

      X[6]a = XXXXXXa
      F[2:4]a = XX(a | X(a | Xa))
      G[2:4]a = XX(a & X(a & Xa))

    The corresponding constructors (for C++ and Python) are
      formula::X(unsigned, formula)
      formula::F(unsigned, unsigned, formula)
      formula::G(unsigned, unsigned, formula)

  - spot::unabbreviate(), used to rewrite away operators such as M or
    W, learned to use some shorter rewritings when an argument (e) is
    a pure eventuality or (u) is purely universal:

      Fe = e
      Gu = u
      f R u = u
      f M e = F(f & e)
      f W u = G(f | u)

  - The twa_graph class has a new dump_storage_as_dot() method
    to show its data structure.  This is more conveniently used
    as aut.show_storage() in a Jupyter notebook.  See
    https://spot.lrde.epita.fr/ipynb/twagraph-internals.html

  - spot::generic_emptiness_check() is a new function that performs
    emptiness checks of twa_graph_ptr (i.e., automata not built
    on-the-fly) with an *arbitrary* acceptance condition.  Its sister
    spot::generic_emptiness_check_scc() can be used to decide the
    emptiness of an SCC.  This is now used by
    twa_graph_ptr::is_empty(), twa_graph_ptr::intersects(), and
    scc_info::determine_unknown_acceptance().

  - The new function spot::to_parity() translates an automaton with
    arbitrary acceptance condition into a parity automaton, based on a
    last-appearance record (LAR) construction.  (It is used by ltlsynt
    but not yet by autfilt or ltl2tgba.)

  - The new function is_liveness() and is_liveness_automaton() can be
    used to check whether a formula or an automaton represents a
    liveness property.

  - Two new functions count_univbranch_states() and
    count_univbranch_edges() can help measuring the amount of
    universal branching in alternating automata.

  Bugs fixed:

  - translate() would incorrectly mark as stutter-invariant
    some automata produced from formulas of the form X(f...)
    where f... is syntactically stutter-invariant.

  - acc_cond::is_generalized_rabin() and
    acc_cond::is_generalized_streett() did not recognize the cases
    where a single generalized pair is used.

  - The pair of acc_cond::mark_t returned by
    acc_code::used_inf_fin_sets(), and the pair (bool,
    vector_rs_pairs) by acc_cond::is_rabin_like() and
    acc_cond::is_streett_like() were not usable in Python.

  - Many object types had __repr__() methods that would return the
    same string as __str__(), contrary to Python usage where repr(x)
    should try to show how to rebuild x.  The following types have
    been changed to follow this convention:
       spot.acc_code
       spot.acc_cond
       spot.atomic_prop_set
       spot.formula
       spot.mark_t
       spot.twa_run (__repr__ shows type and address)
       spot.twa_word (likewise, but _repr_latex_ used in notebooks)

    Note that this you were relying on the fact that Jupyter calls
    repr() to display returned values, you may want to call print()