NEWS 256 KB
Newer Older
1
2
New in spot 2.10.2.dev  (not yet released)

3
4
5
6
7
  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 superflous state.  (Issue #492)
8

9
10
11
12
13
  - 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.

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

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
20
New in spot 2.10.2  (2021-12-03)
21

22
23
24
25
  Bugs fixed:

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

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

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
33
34
  - spot::formula::is_literal() should be const.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
35
New in spot 2.10.1  (2021-11-19)
36

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
  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.
79

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
80
New in spot 2.10  (2021-11-13)
81

82
83
84
85
86
87
88
89
  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.

90
91
  Command-line tools:

92
93
94
95
96
97
  - 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
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
98
      be given and will deduce the value of the other one.
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121

    + 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
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
122
      sub-specifications, the controllers of which can then be glued
123
      together to satisfy the input specification.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
124
      (cf. [finkbeiner.21.nfm] in doc/spot.bib)
125
126
127

    + ltlsynt learned --simplify=no|bisim|bwoa|sat|bisim-sat|bwoa-sat
      to specifies how to simplify the synthesized controler.
128

129
  - ltl2tgba, autfilt, dstar2tgba, and randaut learned a --buchi
130
    option, or -b for short.  This outputs Büchi automata without
131
132
133
134
135
136
137
138
139
140
141
    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.

142
143
  - autfilt learned a --kill-states=NUM[,NUM...] option.

144
145
146
147
148
149
  - 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' ...

150
  Library:
151

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
152
153
154
  - 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).
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171

  - 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.
172
173

    In addition to the previous conversion, we implemented various
174
175
176
177
178
    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,
179
    pinning, and stopping threads inside of parallel model-checking
180
    algorithms.
181

182
183
184
185
    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.
186

187
188
189
190
191
192
193
194
195
196
197
198
  - 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

199
         postprocessor::set_type(postprocessor::GeneralizedBuchi)
200
201
202

    and

203
204
         postprocessor::set_type(postprocessor::BA)

205
    by
206

207
208
209
210
211
212
213
214
215
216
         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).

217
  - Translations for formulas such as FGp1 & FGp2 &...& FGp32 which
218
    used to take ages are now instantaneous.  (Issue #412.)
219

220
  - remove_fin() learned to remove more unnecessary edges by using
221
222
    propagate_marks_vector(), both in the general case and in the
    Rabin-like case.
223

224
225
226
227
  - 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.)

228
229
230
231
232
233
234
  - 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.)

235
  - The parity_game class has been removed, now any twa_graph_ptr that
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
236
    has a "state-player" property is considered to be a game.
237

238
239
240
241
  - 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.

242
243
244
  - print_dot() will display states from player 1 using a diamond
    shape.

245
246
247
  - print_dot() learned to display automata that correspond to Mealy
    machines specifically.

248
249
250
251
252
253
254
255
  - 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

256
257
258
259
260
  - 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.)
261
262

      wdba-det-max   Maximum number of additional states allowed in
263
                     intermediate steps of WDBA-minimization.  If the
264
265
266
                     number of additional states reached in the
                     powerset construction or in the followup products
                     exceeds this value, WDBA-minimization is aborted.
267
                     Defaults to 4096. Set to 0 to disable.  This limit
268
269
270
                     is ignored when -D used or when det-max-states is
                     set.

271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
      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
291
292
293
294
295
296
297
298
                     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.
299

300
301
302
303
304
    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.
305

306
307
308
309
310
311
312
313
314
315
      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.)
316

317
318
319
320
321
322
323
  - 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.

324
  - tgba_powerset() now takes an extra optional argument to specify a
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
325
    list of accepting sinks states if some are known.  Doing so can
326
327
    cut the size of the powerset automaton by 2^|sinks| in favorable
    cases.
328

329
330
331
  - twa_graph::merge_edges() had its two passes swapped.  Doing so
    improves the determinism of some automata.

332
333
334
335
  - 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.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
336
337
338
339
340
341
342
343
344
345
  - 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)).
346

347
348
349
350
351
352
  - 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)

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
353
354
355
356
357
  - 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.
358

359
360
361
362
  - 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.
363
364
    Additionally, this function now returns the number of states that
    have been merged (and therefore removed from the automaton).
365

366
  - spot::zielonka_tree and spot::acd are new classes that implement the
367
368
369
370
371
    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.
372

373
374
  Python:

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
375
376
377
378
  - 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.

379
  - Bindings for functions related to synthesis and aig-circuits.
380
    See https://spot.lrde.epita.fr/ipynb/synthesis.html
381

382
  - spot::twa::prop_set was previously absent from the Python
383
384
385
386
    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).
387

388
389
  Bugs fixed:

390
391
  - tgba_determinize() could create parity automata using more colors
    than necessary.  (Related to issue #298)
392

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
393
394
395
396
397
  - 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.

398
399
400
401
402
403
  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.
404

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
405
New in spot 2.9.8 (2021-08-10)
406

407
408
409
410
  Documentation:

  - Mention the conda-forge package.

411
412
413
414
  Bugs fixed:

  - left->intersacting_run(right) could return a run with incorrect
    colors (likely not corresponding to any existing transition of
415
416
417
418
419
420
421
422
    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.

423

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
424
New in spot 2.9.7 (2021-05-12)
425

426
  Bugs fixed:
427

428
429
430
  - Some formulas using ->, <->, or xor were not properly detected as
    purely universal or pure eventualities.

431
432
433
  - autfilt --keep-states=... could incorrectly mention --mask-acc
    when diagnosing errors.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
434
435
  - Work around GraphViz issue 1931, causing spurious failures in the
    test suite.
436

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
437
  - Miscelaneous documentation fixes.
438

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
439
New in spot 2.9.6 (2021-01-18)
440

441
442
443
444
445
  Build:

  - Build scripts are now compatible with Autoconf 2.70 (Issue #447)
    and require at least Autoconf 2.69 (released in 2012).

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
446
  - Debian builds use updated standards.
447

448
449
  Bugs fixed:

450
451
452
  - twa_graph::merge_edges() could fail to merge two transitions if the
    destination transition was the first of the automaton.  (Issue #441)

453
454
455
456
  - On non-deterministic automata, iterated_simulations() was
    performing an (unnecessary) second iteration even when the first
    one failed to reduce the automaton.  (Issue #442)

457
458
  - When passed an incomplete automaton as input, tgba_determinize()
    would sometimes produce a complete automaton but incorrectly mark
459
460
461
462
463
464
    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.
465

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
466
New in spot 2.9.5 (2020-11-19)
467

468
469
  Bugs fixed:

470
471
472
473
  - Fix multiple spurious test suite failures on Darwin
    (Issues #426, #427, #428, #429) or when the
    Pandas package was not installed.

474
475
  - The filename python/spot/aux.py caused a problem on Windows and
    has been renamed.  Existing "import spot.aux" statements should
476
477
478
479
480
    *not* be updated.  (Issue #437)

  - Fix memory leak in minimize_wdba() when determinization is aborted
    because an output_aborter is passed.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
481
  - Distribution used to contain unnecessary large SVG files (Issue #422)
482

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
483
New in spot 2.9.4 (2020-09-07)
484

485
486
487
  Bugs fixed:

  - Handle xor and <-> in a more natural way when translating
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
488
489
490
    LTL formulas to generic acceptance conditions.

  - Multiple typos in documentation, --help texts, or error messages.
491

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
492
New in spot 2.9.3 (2020-07-22)
493

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
494
  Bug fixed:
495

496
  - Completely fix the ltlcross issue mentioned in previous release.
497

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
498
New in spot 2.9.2 (2020-07-21)
499

500
501
502
  Bugs fixed:

  - ltlcross --csv=... --product=N with N>0 could output spurious
503
    diagnostics claiming that words were rejected when evaluating
504
505
506
507
508
    the automaton on state-space.

  - spot::scc_info::determine_unknown_acceptance() now also update the
    result of spot::scc_info::one_accepting_scc().

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
509
New in spot 2.9.1 (2020-07-15)
510

511
512
513
514
515
516
517
  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).

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
518
  - Option '-x wdba-minimize=N' used to accept N=0 (off), or N=1 (on).
519
520
521
522
523
524
525
526
527
528
    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.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
529
530
531
  - ltlsynt learned --algo=ps to use the default conversion to
    deterministic parity automata (the same as ltl2tgba -DP'max odd').

532
533
534
535
  - 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.

536
537
  Library:

538
  - product_xor() and product_xnor() are two new versions of the
539
    synchronized product.  They only work with operands that are
540
541
542
543
    deterministic automata, and build automata whose language are
    respectively the symmetric difference of the operands, and the
    complement of that.

544
545
546
547
548
  - 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.
549

550
551
552
  - remove_fin() learned a trick to remove some superfluous
    transitions.

553
554
  Bugs fixed:

555
556
  - Work around undefined behavior reported by clang 10.0.0's UBsan.

557
558
559
560
561
562
  - 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.

563
564
  - simplify_acceptance() missed some patterns it should have been
    able to simplify.  For instance Fin(0)&(Fin(1)|Fin(2)|Fin(4))
Florian Renkin's avatar
Florian Renkin committed
565
    should simplify to Fin(1)|Fin(2)|Fin(4) after adding {1,2,4} to
566
567
568
    every place where 0 occur, and then the acceptance would be
    renumbered to Fin(0)|Fin(1)|Fin(2).  This is now fixed.

569
570
571
  - Improve ltldo diagnostics to fix spurious test-suite failure on
    systems with antique GNU libc.

572
573
574
575
576
  - 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().

577
578
579
580
581
  - 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.

582
583
584
  - scc_info::edges_of() and scc_info::inner_edges_of() now correctly
    honor any filter passed to scc_info.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
585
New in spot 2.9 (2020-04-30)
586

587
588
589
590
591
592
593
594
595
596
597
598
599
600
  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}"

601
  - autfilt learned the --partial-degeneralize option, to remove
602
    conjunctions of Inf, or disjunctions of Fin that appears in
603
604
    arbitrary conditions.

605
606
607
608
  - 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).

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
609
  - When running translators, ltlcross will now display {names} when
610
611
    supplied.

612
613
614
615
  - 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.

616
617
618
619
  - 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.

620
621
622
  - ltlsynt --algo=lar uses the new version of to_parity() mentionned
    below.  The old version is available via --algo=lar.old

623
624
625
  - ltlsynt learned --csv=FILENAME, to record some statistics about
    the duration of its different phases.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
626
627
628
629
630
631
  - 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.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
632
633
634
635
636
637
638
639
640
  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).

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
641
    To accommodate this, this version introduces a new operator
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
642
643
644
645
646
647
648
649
650
651
652
653
654
    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
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
655
    the same way, since there is no difference between X and X[!] over
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
656
657
658
659
660
661
    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.

662
663
664
665
666
667
668
669
670
671
  - 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)

672
  - partial_degeneralize() is a new function performing partial
673
674
    degeneralization to get rid of conjunctions of Inf terms, or
    disjunctions of Fin terms in acceptance conditions.
675

676
677
  - simplify_acceptance_here() and simplify_acceptance() learned to
    simplify subformulas like Fin(i)&Fin(j) or Inf(i)|Inf(j), or some
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
678
679
680
    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
681
682
    appeared.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
683
684
685
686
687
  - 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().

688
  - propagate_marks_vector() and propagate_marks_here() are helper
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
689
    functions for propagating marks on the automaton: ignoring
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
690
691
692
693
694
695
696
    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.
697

698
699
700
701
702
703
  - 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).

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
704
705
  - to_parity() has been rewritten. It now combines several strategies
    for paritizing automata with any acceptance condition.
706

707
708
709
710
  - 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.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
711
  - print_dot()'s default was changed to use circles for automata with
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
712
713
714
715
716
717
    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.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
718
719
720
  - The generic emptiness check has been slightly improved (doing
    fewer recursive calls in the worst case).

721
722
723
724
725
726
727
  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().
728

729
730
731
  - The twa_graph::is_alternating() and digraph::is_alternating() methods,
    deprecated in Spot 2.3.1 (2017-02-20), have been removed.

732
733
734
735
736
  Bugs fixed:

  - Relabeling automata could introduce false edges.  Those are now
    removed.

737
738
739
  - Emptiness checks, and scc_info should now ignore edges labeled
    with false.

740
741
742
  - relabel_bse() could incorrectly relabel Boolean subformulas that
    had some atomic propositions in common.

743
New in spot 2.8.7 (2020-03-13)
744

745
746
747
  Bugs fixed:

  - Building a product between two complete automata where one operand
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
748
    had false acceptance could create an incomplete automaton
749
750
751
    incorrectly tagged as complete, causing the print_hoa() function
    to raise an exception.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
752
753
754
  - autfilt --uniq was not considering differences in acceptance
    conditions or number of states when discarding automata.

755
756
757
758
759
760
  - 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.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
761
762
763
764
765
766
767
768
769
770
771
772
  - 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).

773
774
775
  - ltlcross was not diagnosing write errors associated to
    options --grind=FILENAME and --save-bogus=FILENAME.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
776
New in spot 2.8.6 (2020-02-19)
777

778
779
  Bugs fixed:

780
781
782
783
  - calling spot.translate() with two conflicting preferences like
    spot.translate(..., 'det', 'any') triggered a syntax error in the
    Python code to handle this error.

784
785
786
787
788
  - 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).

789
790
791
  - Some formulas with Boolean sub-formulas equivalent to true or
    false could be translated into automata with false labels.

792
793
794
795
  - 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.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
796
New in spot 2.8.5 (2020-01-04)
797

798
799
800
801
802
  Bugs fixed:

  - ltl2tgba -B could return automata with "t" acceptance, instead
    of the expected Inf(0).

803
804
805
806
807
808
809
810
811
  - 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.

812
New in spot 2.8.4 (2019-12-08)
813

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
814
815
816
817
818
819
820
821
822
  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.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
823
824
825
  - Work around a small difference between Python 3.7 and 3.8, causing
    spurious failures of the test suite.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
826
New in spot 2.8.3 (2019-11-06)
827

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
828
829
830
  Build:

  - Minor portabilities improvements with C++17 deprecations.
831

832
833
834
835
836
837
  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.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
838
839
840
  - Work around GraphViz bug #1605 in Jupyter notebooks.
    https://gitlab.com/graphviz/graphviz/issues/1605

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
841
New in spot 2.8.2 (2019-09-27)
842

843
844
845
846
  Command-line tools:

  - ltl2tgba and ltldo learned a --negate option.

847
848
849
850
851
  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".
852

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
853
854
855
856
  - The numbering of nodes in the AIGER output of ltlsynt was
    architecture dependent.

  - Various compilation issues.  In particular, this release is the
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
857
    first one that can be compiled (and pass tests) on a Raspberry PI.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
858

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
859
New in spot 2.8.1 (2019-07-18)
860

861
862
863
864
  Command-line tools:

  - genltl learned --pps-arbiter-standard and --pps-arbiter-strict.

865
866
867
868
869
870
  - 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.

871
872
873
874
875
876
877
  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".
878

879
880
881
882
  - Work around Emacs bug #34341 when rebuilding documentation on a
    system with Emacs <26.3, GNU TLS >= 3.6, and without ESS or with
    an obsolete org-mode installed.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
883
New in spot 2.8 (2019-07-10)
884

885
886
887
888
889
  Command-line tools:

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

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

893
894
895
896
897
898
899
900
901
  - 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.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
902
  - ltlcross will now skip unnecessary cross-checks and
903
904
905
    consistency-checks (they are unnecessary when all automata
    could be complemented and statistics were not required).

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
906
  - genaut learned --m-nba=N to generate Max Michel's NBA family.
907
908
    (NBAs with N+1 states whose determinized have at least N! states.)

909
910
911
  - 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
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
912
    among "Inf(0)", "t", or "f", and persistence properties have an
913
914
    acceptance condition among "Fin(0)", "t", or "f".

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

919
920
921
  Documentation:

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

924
925
926
927
928
  Library:

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

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

932
933
934
935
936
937
938
  - 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.)

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
939
940
  - simulation-based reductions has learned another trick to better
    merge states from transient SCCs.
941

942
943
944
  - 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.
945

946
947
948
949
950
  - 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.)

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
951
  - There is a new spot::scc_and_mark_filter object that simplifies the
952
953
954
955
956
    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.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
957
958
959
960
  - 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.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
961
962
963
964
  - 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.
965

966
967
968
969
970
971
972
973
974
975
976
977
978
979
  - 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.

980
981
982
983
984
985
986
  - 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.

987
988
  - 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
989
990
    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.
991
    The formula::sugar_delay() function implements this SVA operator in
992
993
    terms of the existing PSL operators.  ##[+] and ##[*] are sugar
    for ##[1:$] and ##[0:$].
994

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

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