NEWS 257 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
New in spot 2.10.5  (2022-05-03)
2

3
4
5
6
7
  Bugs fixed:

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

8
9
10
11
12
13
14
15
16
17
  - 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
18
19
    compilation on OpenBSD.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
20
21
22
  - Do not use the seq command in test cases, it is not available
    everywhere.

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

26
27
28
29
30
31
  - Simplify Debian instructions for LTO build to work around newer
    libtool version.

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
32
New in spot 2.10.4  (2022-02-01)
33

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
34
  Bug fixed:
35
36
37
38
39
40

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
42
New in spot 2.10.3  (2022-01-15)
43

44
45
46
47
  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
48
    SCC, sbacc() could output a superfluous state.  (Issue #492)
49

50
51
52
53
54
  - 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.

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

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

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

64
65
66
67
68
  - Mealy machine resulting from SAT-based minimization could differ
    on architectures with different hash tables implementations.

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

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

71
72
73
74
  Bugs fixed:

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

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

79
80
81
  - 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
82
83
  - spot::formula::is_literal() should be const.

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
  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.
128

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

131
132
133
134
135
136
137
138
  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.

139
140
  Command-line tools:

141
142
143
144
145
146
  - 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
147
      be given and will deduce the value of the other one.
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170

    + 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
171
      sub-specifications, the controllers of which can then be glued
172
      together to satisfy the input specification.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
173
      (cf. [finkbeiner.21.nfm] in doc/spot.bib)
174
175
176

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

178
  - ltl2tgba, autfilt, dstar2tgba, and randaut learned a --buchi
179
    option, or -b for short.  This outputs Büchi automata without
180
181
182
183
184
185
186
187
188
189
190
    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.

191
192
  - autfilt learned a --kill-states=NUM[,NUM...] option.

193
194
195
196
197
198
  - 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' ...

199
  Library:
200

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
201
202
203
  - 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).
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220

  - 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.
221
222

    In addition to the previous conversion, we implemented various
223
224
225
226
227
    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,
228
    pinning, and stopping threads inside of parallel model-checking
229
    algorithms.
230

231
232
233
234
    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.
235

236
237
238
239
240
241
242
243
244
245
246
247
  - 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

248
         postprocessor::set_type(postprocessor::GeneralizedBuchi)
249
250
251

    and

252
253
         postprocessor::set_type(postprocessor::BA)

254
    by
255

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

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

269
  - remove_fin() learned to remove more unnecessary edges by using
270
271
    propagate_marks_vector(), both in the general case and in the
    Rabin-like case.
272

273
274
275
276
  - 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.)

277
278
279
280
281
282
283
  - 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.)

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

287
288
289
290
  - 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.

291
292
293
  - print_dot() will display states from player 1 using a diamond
    shape.

294
295
296
  - print_dot() learned to display automata that correspond to Mealy
    machines specifically.

297
298
299
300
301
302
303
304
  - 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

305
306
307
308
309
  - 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.)
310
311

      wdba-det-max   Maximum number of additional states allowed in
312
                     intermediate steps of WDBA-minimization.  If the
313
314
315
                     number of additional states reached in the
                     powerset construction or in the followup products
                     exceeds this value, WDBA-minimization is aborted.
316
                     Defaults to 4096. Set to 0 to disable.  This limit
317
318
319
                     is ignored when -D used or when det-max-states is
                     set.

320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
      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
340
341
342
343
344
345
346
347
                     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.
348

349
350
351
352
353
    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.
354

355
356
357
358
359
360
361
362
363
364
      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.)
365

366
367
368
369
370
371
372
  - 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.

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

378
379
380
  - twa_graph::merge_edges() had its two passes swapped.  Doing so
    improves the determinism of some automata.

381
382
383
384
  - 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
385
386
387
388
389
390
391
392
393
394
  - 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)).
395

396
397
398
399
400
401
  - 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
402
403
404
405
406
  - 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.
407

408
409
410
411
  - 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.
412
413
    Additionally, this function now returns the number of states that
    have been merged (and therefore removed from the automaton).
414

415
  - spot::zielonka_tree and spot::acd are new classes that implement the
416
417
418
419
420
    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.
421

422
423
  Python:

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
424
425
426
427
  - 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.

428
  - Bindings for functions related to synthesis and aig-circuits.
429
    See https://spot.lrde.epita.fr/ipynb/synthesis.html
430

431
  - spot::twa::prop_set was previously absent from the Python
432
433
434
435
    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).
436

437
438
  Bugs fixed:

439
440
  - tgba_determinize() could create parity automata using more colors
    than necessary.  (Related to issue #298)
441

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
442
443
444
445
446
  - 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.

447
448
449
450
451
452
  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.
453

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

456
457
458
459
  Documentation:

  - Mention the conda-forge package.

460
461
462
463
  Bugs fixed:

  - left->intersacting_run(right) could return a run with incorrect
    colors (likely not corresponding to any existing transition of
464
465
466
467
468
469
470
471
    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.

472

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

475
  Bugs fixed:
476

477
478
479
  - Some formulas using ->, <->, or xor were not properly detected as
    purely universal or pure eventualities.

480
481
482
  - autfilt --keep-states=... could incorrectly mention --mask-acc
    when diagnosing errors.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
483
484
  - Work around GraphViz issue 1931, causing spurious failures in the
    test suite.
485

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
486
  - Miscelaneous documentation fixes.
487

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

490
491
492
493
494
  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
495
  - Debian builds use updated standards.
496

497
498
  Bugs fixed:

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

502
503
504
505
  - On non-deterministic automata, iterated_simulations() was
    performing an (unnecessary) second iteration even when the first
    one failed to reduce the automaton.  (Issue #442)

506
507
  - When passed an incomplete automaton as input, tgba_determinize()
    would sometimes produce a complete automaton but incorrectly mark
508
509
510
511
512
513
    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.
514

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

517
518
  Bugs fixed:

519
520
521
522
  - Fix multiple spurious test suite failures on Darwin
    (Issues #426, #427, #428, #429) or when the
    Pandas package was not installed.

523
524
  - The filename python/spot/aux.py caused a problem on Windows and
    has been renamed.  Existing "import spot.aux" statements should
525
526
527
528
529
    *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
530
  - Distribution used to contain unnecessary large SVG files (Issue #422)
531

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

534
535
536
  Bugs fixed:

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

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

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
543
  Bug fixed:
544

545
  - Completely fix the ltlcross issue mentioned in previous release.
546

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

549
550
551
  Bugs fixed:

  - ltlcross --csv=... --product=N with N>0 could output spurious
552
    diagnostics claiming that words were rejected when evaluating
553
554
555
556
557
    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
558
New in spot 2.9.1 (2020-07-15)
559

560
561
562
563
564
565
566
  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
567
  - Option '-x wdba-minimize=N' used to accept N=0 (off), or N=1 (on).
568
569
570
571
572
573
574
575
576
577
    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
578
579
580
  - ltlsynt learned --algo=ps to use the default conversion to
    deterministic parity automata (the same as ltl2tgba -DP'max odd').

581
582
583
584
  - 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.

585
586
  Library:

587
  - product_xor() and product_xnor() are two new versions of the
588
    synchronized product.  They only work with operands that are
589
590
591
592
    deterministic automata, and build automata whose language are
    respectively the symmetric difference of the operands, and the
    complement of that.

593
594
595
596
597
  - 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.
598

599
600
601
  - remove_fin() learned a trick to remove some superfluous
    transitions.

602
603
  Bugs fixed:

604
605
  - Work around undefined behavior reported by clang 10.0.0's UBsan.

606
607
608
609
610
611
  - 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.

612
613
  - 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
614
    should simplify to Fin(1)|Fin(2)|Fin(4) after adding {1,2,4} to
615
616
617
    every place where 0 occur, and then the acceptance would be
    renumbered to Fin(0)|Fin(1)|Fin(2).  This is now fixed.

618
619
620
  - Improve ltldo diagnostics to fix spurious test-suite failure on
    systems with antique GNU libc.

621
622
623
624
625
  - 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().

626
627
628
629
630
  - 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.

631
632
633
  - 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
634
New in spot 2.9 (2020-04-30)
635

636
637
638
639
640
641
642
643
644
645
646
647
648
649
  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}"

650
  - autfilt learned the --partial-degeneralize option, to remove
651
    conjunctions of Inf, or disjunctions of Fin that appears in
652
653
    arbitrary conditions.

654
655
656
657
  - 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
658
  - When running translators, ltlcross will now display {names} when
659
660
    supplied.

661
662
663
664
  - 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.

665
666
667
668
  - 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.

669
670
671
  - ltlsynt --algo=lar uses the new version of to_parity() mentionned
    below.  The old version is available via --algo=lar.old

672
673
674
  - ltlsynt learned --csv=FILENAME, to record some statistics about
    the duration of its different phases.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
675
676
677
678
679
680
  - 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
681
682
683
684
685
686
687
688
689
  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
690
    To accommodate this, this version introduces a new operator
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
691
692
693
694
695
696
697
698
699
700
701
702
703
    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
704
    the same way, since there is no difference between X and X[!] over
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
705
706
707
708
709
710
    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.

711
712
713
714
715
716
717
718
719
720
  - 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)

721
  - partial_degeneralize() is a new function performing partial
722
723
    degeneralization to get rid of conjunctions of Inf terms, or
    disjunctions of Fin terms in acceptance conditions.
724

725
726
  - 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
727
728
729
    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
730
731
    appeared.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
732
733
734
735
736
  - 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().

737
  - propagate_marks_vector() and propagate_marks_here() are helper
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
738
    functions for propagating marks on the automaton: ignoring
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
739
740
741
742
743
744
745
    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.
746

747
748
749
750
751
752
  - 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
753
754
  - to_parity() has been rewritten. It now combines several strategies
    for paritizing automata with any acceptance condition.
755

756
757
758
759
  - 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
760
  - print_dot()'s default was changed to use circles for automata with
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
761
762
763
764
765
766
    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
767
768
769
  - The generic emptiness check has been slightly improved (doing
    fewer recursive calls in the worst case).

770
771
772
773
774
775
776
  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().
777

778
779
780
  - The twa_graph::is_alternating() and digraph::is_alternating() methods,
    deprecated in Spot 2.3.1 (2017-02-20), have been removed.

781
782
783
784
785
  Bugs fixed:

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

786
787
788
  - Emptiness checks, and scc_info should now ignore edges labeled
    with false.

789
790
791
  - relabel_bse() could incorrectly relabel Boolean subformulas that
    had some atomic propositions in common.

792
New in spot 2.8.7 (2020-03-13)
793

794
795
796
  Bugs fixed:

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

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

804
805
806
807
808
809
  - 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
810
811
812
813
814
815
816
817
818
819
820
821
  - 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).

822
823
824
  - ltlcross was not diagnosing write errors associated to
    options --grind=FILENAME and --save-bogus=FILENAME.

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

827
828
  Bugs fixed:

829
830
831
832
  - calling spot.translate() with two conflicting preferences like
    spot.translate(..., 'det', 'any') triggered a syntax error in the
    Python code to handle this error.

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

838
839
840
  - Some formulas with Boolean sub-formulas equivalent to true or
    false could be translated into automata with false labels.

841
842
843
844
  - 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
845
New in spot 2.8.5 (2020-01-04)
846

847
848
849
850
851
  Bugs fixed:

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

852
853
854
855
856
857
858
859
860
  - 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.

861
New in spot 2.8.4 (2019-12-08)
862

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
863
864
865
866
867
868
869
870
871
  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
872
873
874
  - 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
875
New in spot 2.8.3 (2019-11-06)
876

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
877
878
879
  Build:

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

881
882
883
884
885
886
  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
887
888
889
  - Work around GraphViz bug #1605 in Jupyter notebooks.
    https://gitlab.com/graphviz/graphviz/issues/1605

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

892
893
894
895
  Command-line tools:

  - ltl2tgba and ltldo learned a --negate option.

896
897
898
899
900
  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".
901

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
902
903
904
905
  - 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
906
    first one that can be compiled (and pass tests) on a Raspberry PI.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
907

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

910
911
912
913
  Command-line tools:

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

914
915
916
917
918
919
  - 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.

920
921
922
923
924
925
926
  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".
927

928
929
930
931
  - 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
932
New in spot 2.8 (2019-07-10)
933

934
935
936
937
938
  Command-line tools:

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

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

942
943
944
945
946
947
948
949
950
  - 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
951
  - ltlcross will now skip unnecessary cross-checks and
952
953
954
    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
955
  - genaut learned --m-nba=N to generate Max Michel's NBA family.
956
957
    (NBAs with N+1 states whose determinized have at least N! states.)

958
959
960
  - 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
961
    among "Inf(0)", "t", or "f", and persistence properties have an
962
963
    acceptance condition among "Fin(0)", "t", or "f".

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

968
969
970
  Documentation:

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

973
974
975
976
977
  Library:

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

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

981
982
983
984
985
986
987
  - 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
988
989
  - simulation-based reductions has learned another trick to better
    merge states from transient SCCs.
990

991
992
993
  - 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.
994

995
996
997
998
999
  - 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
1000
  - There is a new spot::scc_and_mark_filter object that simplifies the
1001
1002
1003
1004
1005
    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
1006
1007
1008
1009
  - 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
1010
1011
1012
1013
  - 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.
1014

1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
  - 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.

1029
1030
1031
1032
1033
1034
1035
  - 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.

1036
1037
  - 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
1038
1039
    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.
1040
    The formula::sugar_delay() function implements this SVA operator in
1041
1042
    terms of the existing PSL operators.  ##[+] and ##[*] are sugar
    for ##[1:$] and ##[0:$].
1043

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

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

1050
  - The LTL simplifier learned the following rules:
1051
    F(G(a | Fb)) = FGa | GFb  (if option "favor_event_univ")
1052
    G(F(a | Gb)) = GFa | FGb  (if option "favor_event_univ")
1053
1054
    F(G(a & Fb) = FGa & GFb   (unless option "reduce_size_strictly")
    G(F(a & Gb)) = GFa & FGb  (unless option "reduce_size_strictly")
1055
1056
    GF(f) = GF(dnf(f))        (unless option "reduce_size_strictly")
    FG(f) = FG(cnf(f))        (unless option "reduce_size_strictly")
1057
1058
1059
1060
1061
1062
1063
1064
    (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
1065

1066
1067
  - cleanup_parity() and colorize_parity() were cleaned up a bit,
    resulting in fewer colors used in some cases.  In particular,
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1068
    colorize_parity() learned that coloring transient edges does not
1069
1070
    require the introduction of a new color.

1071
1072
1073
1074
1075
1076
  - 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.

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

1080
1081
1082
1083
1084
1085
1086
  - 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.

1087
  Deprecation notices:
1088

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1089
  - The virtual function twa::intersecting_run() no longer takes a
1090
1091
1092
1093
1094
1095
    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.

1096
1097
1098
1099
1100
  - 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.

1101
1102
  Bugs fixed:

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1103
  - The gf_guarantee_to_ba() is relying on an in-place algorithm that
1104
1105
1106
    could produce a different number of edges for the same input in
    two different transition order.

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1112
New in spot 2.7.5 (2019-06-05)
1113

1114
1115
1116
  Build:

  - Although the Python bindings in this release are still done with
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1117
    Swig3.0, the code has been updated to be compatible with Swig4.0.
1118

1119
1120
1121
1122
1123
1124
  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.
1125

1126
1127
  Bugs fixed:

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1128
  - spot::translator was not applying Boolean sub-formula rewriting
1129
    by default unless a spot::option_map was passed.  This caused some
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1130
    C++ code for translating certain formulas to be noticeably slower
1131
1132
    than the equivalent call to the ltl2tgba binary.

1133
1134
1135
1136
  - 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.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1137
New in spot 2.7.4 (2019-04-27)
1138

1139
1140
1141
1142
1143
  Bugs fixed:

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

1144
1145
1146
1147
1148
  - 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.

1149
1150
1151
1152
  - 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.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1153
New in spot 2.7.3 (2019-04-19)
1154

1155
1156
1157
1158
1159
1160
  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.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1161
  - Fix serious typo in remove_alternation() causing incorrect
1162
1163
    output for some VWAA.  Bug introduced in Spot 2.6.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1164
1165
1166
1167
  Documentation:

  - Multiple typos and minor updates.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1168
1169
1170
1171
1172
1173
1174
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.
1175

1176
1177
1178
1179
  Documentation:

  - A new page shows how to create explicit Kripke structures in C++
    and Python.  See https://spot.lrde.epita.fr/tut52.html
1180
1181
1182
  - 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
1183

1184
1185
1186
1187
1188
  Build:

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1189
New in spot 2.7.1 (2019-02-14)
1190

1191
  Build:
1192

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1193
  - Work around GCC bug #89303 that causes memory leaks and std::weak_bad_ptr
1194
    exceptions when Spot is compiled with the version of g++ 8.2 currently
1195
    distributed by Debian unstable (starting with g++ 8.2.0-15).
1196

1197
1198
1199
  Python:

  - The following methods of spot::bdd_dict are now usable in Python when
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1200
    fine control over the lifetime of associations between BDD variables
1201
1202
1203
1204
1205
1206
1207
    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)

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1208
1209
  - Better support for explicit Kripke structures:
    - the kripke_graph type now has Python bindings
1210
1211
1212
1213
1214
1215
1216
1217
1218
    - 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.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1219
1220
  - kripke_graph_ptr objects now honor any "state-names" property
    when formatting states.
1221

1222
1223
1224
1225
1226
  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.
1227

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

1232
1233
1234
1235
  - 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.

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

1239
1240
  - The product_susp() function used to multiply an automaton with a
    suspendable automaton could incorrectly build transition-based
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1241
    automata when multiplying two state-based automata.  This caused
1242
    ltl2tgba to emit error messages such as: "automaton has
1243
    transition-based acceptance despite prop_state_acc()==true".
1244

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1245
New in spot 2.7 (2018-12-11)
1246

1247
1248
1249
1250
1251
1252
1253
1254
  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.
1255
    --algo=lar    translate the formula to a deterministic automaton
1256
1257
1258
1259
1260
1261
                  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.

1262
1263
  - ltlfilt learned --liveness to match formulas representing liveness
    properties.
1264

1265
1266
1267
1268
1269
  - 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.

1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
  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.)

1280
1281
1282
1283
  - 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.

1284
1285
  Library:

1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
  - 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)
1299

1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
  - 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)

1310
1311
1312
1313
1314
  - 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

1315
1316
1317
1318
  - 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
1319
1320
1321
    emptiness of an SCC.  This is now used by
    twa_graph_ptr::is_empty(), twa_graph_ptr::intersects(), and
    scc_info::determine_unknown_acceptance().
1322

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1323
1324
1325
1326
  - 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.)
1327

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

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

1336
1337
  Bugs fixed:

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

1342
1343
  - acc_cond::is_generalized_rabin() and
    acc_cond::is_generalized_streett() did not recognize the cases
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1344
    where a single generalized pair is used.
1345

1346
  - The pair of acc_cond::mark_t returned by
1347
1348
1349
    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.
1350

1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
1361
1362
1363
1364
  - 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()
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1365