NEWS 268 KB
Newer Older
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1
New in spot 2.11.2  (2022-10-26)
2

3
4
5
6
7
8
9
  Command-line tools:

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

10
11
12
13
14
15
  Library:

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

16
17
18
  Bugs fixed:

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
23
New in spot 2.11.1  (2022-10-10)
24

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
25
26
27
28
  Bugs fixed:

  - Fix a build issue preventing the update of website (issue #516).
  - Fix a compilation error with clang-14 on FreeBSD (issue #515).
29

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
30
New in spot 2.11  (2022-10-08)
31

32
33
  Build:

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
34
  - configure will now diagnose situations where Python bindings will
35
36
37
38
    be installed in a directory that is not part of Python's search
    path.  A new configure option --with-pythondir can be used to
    modify this installation path.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
39
40
41
42
43
44
45
46
47
  - A new configure option --enable-pthread enables the compilation of
    Spot with -pthread, and render available the parallel version of
    some algorithms.  If Spot is compiled with -pthread enabled, any
    user linking with Spot should also link with the pthread library.
    In order to not break existing build setups using Spot, this
    option is currently disabled by default in this release.  We plan
    to turn it on by default in some future release.  Third-party
    project using Spot may want to start linking with -pthread in
    prevision for this change.
48

49
50
51
  Command-line tools:

  - autfilt has a new options --aliases=drop|keep to specify
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
52
    if the HOA printer should attempt to preserve aliases
53
54
    present in the HOA input.  This defaults to "keep".

55
56
57
  - autfilt has a new --to-finite option, illustrated on
    https://spot.lrde.epita.fr/tut12.html

58
59
60
61
62
  - ltlfilt has a new --sonf option to produce a formula's Suffix
    Operator Normal Form, described in [cimatti.06.fmcad].  The
    associated option --sonf-aps allows listing the newly introduced
    atomic propositions.

63
64
65
  - autcross learned a --language-complemented option to assist in the
    case one is testing tools that complement automata.  (issue #504).

66
  - ltlsynt has a new option --tlsf that takes the filename of a TLSF
67
68
69
    specification and calls syfco (which must be installed) to convert
    it into an LTL formula.

70
71
72
  - ltlsynt has a new option --from-pgame that takes a parity game in
    extended HOA format, as used in the Synthesis Competition.

73
74
75
76
77
78
79
80
81
82
  - ltlsynt has a new option --hide-status to hide the REALIZABLE or
    UNREALIZABLE output expected by SYNTCOMP.  (This line is
    superfluous, because the exit status of ltlsynt already indicate
    whether the formula is realizable or not.)

  - ltlsynt has a new option --dot to request GraphViz output instead
    of most output.  This works for displaying Mealy machines, games,
    or AIG circuits.  See https://spot.lrde.epita.fr/ltlsynt.html for
    examples.

83
84
85
86
87
  - genaut learned the --cyclist-trace-nba and --cyclist-proof-dba
    options.  Those are used to generate pairs of automata that should
    include each other, and are used to show a regression (in speed)
    present in Spot 2.10.x and fixed in 2.11.

88
89
90
91
92
93
94
  - genltl learned --eil-gsi to generate a familly a function whose
    translation and simplification used to be very slow.  In particular

       genltl --eil-gsi=23 | ltlfilt --from-ltlf | ltl2tgba

     was reported as taking 9 days.  This is now instantaneous.

95
96
  Library:

97
98
99
100
  - The new function suffix_operator_normal_form() implements
    transformation of formulas to Suffix Operator Normal Form,
    described in [cimatti.06.fmcad].

101
102
103
104
105
106
107
108
109
110
  - "original-classes" is a new named property similar to
    "original-states".  It maps an each state to an unsigned integer
    such that if two classes are in the same class, they are expected
    to recognize the same language.  The "original-states" should be
    prefered property when that integer correspond to some actual
    state.

  - tgba_determinize() learned to fill the "original-classes" property.
    States of the determinized automaton that correspond to the same
    subset of states of the original automaton belong to the same
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
111
112
    class.  Filling this property is only done on demand as it inccurs
    a small overhead.
113
114

  - sbacc() learned to take the "original-classes" property into
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
115
    account and to preserve it.
116

117
118
119
120
  - The HOA parser and printer learned to map the synthesis-outputs
    property of Spot to the controllable-AP header for the Extended
    HOA format used in SyntComp.   https://arxiv.org/abs/1912.05793

121
122
123
124
  - The automaton parser learned to parse games in the PGSolver format.
    See the bottom of https://spot.lrde.epita.fr/ipynb/games.html for
    an example.

125
126
127
128
129
130
131
132
  - "aliases" is a new named property that is filled by the HOA parser
    using the list of aliases declared in the HOA file, and then used
    by the HOA printer on a best-effort basis.  Aliases can be used to
    make HOA files more compact or more readable.  But another
    possible application is to use aliases to name letters of a 2^AP
    alphabet, in applications where using atomic propositions is
    inconvenient.

133
134
135
  - print_dot() learned option "@" to display aliases, as discussed
    above.

136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
  - to_finite() is a new function that help interpreting automata
    build from LTLf formula using the from_ltlf() function.  It replace
    the previously suggested method of removing and atomic proposition
    and simpifying automata, that failed to deal with states without
    successors.  See updated https://spot.lrde.epita.fr/tut12.html

  - the HOA parser learned to not ignore self-loops labeled with [f]
    and to turn any state that have colors but no outgoing transitions
    into a state with a [f] self-loop.  This helps dealing with
    automata containing states without successors, as in the output of
    to_finite().

  - purge_dead_states() will now also remove edges labeled by false
    (except self-loops).

151
152
153
154
155
156
157
158
159
  - When parsing formulas with a huge number of operands for an n-ary
    operator (for instance 'p1 | p2 | ... | p1000') the LTL parser
    would construct that formula two operand at a time, and the
    formula constructor for that operator would be responsible for
    inlining, sorting, deduplicating, ... all operands at each step.
    This resulted in a worst-than-quadratic slowdown.  This is now
    averted in the parser by delaying the construction of such n-ary
    nodes until all children are known.

160
161
162
  - complement() used to always turn tautological acceptance conditions
    into Büchi.  It now only does that if the automaton is modified.

163
164
  - The zielonka_tree construction was optimized using the same
    memoization trick that is used in ACD.  Additionally it can now be
165
    run with additional options to abort when the tree as an unwanted
166
167
    shape, or to turn the tree into a DAG.

168
169
170
171
172
  - contains() can now take a twa as a second argument, not just a
    twa_graph.  This allows for instance to do contains(ltl, kripke)
    to obtain a simple model checker (that returns true or false,
    without counterexample).

173
174
175
  - degeneralize() and degeneralize_tba() learned to work on
    generalized-co-Büchi as well.

176
177
178
179
  - product() learned that the product of two co-Büchi automata
    is a co-Büchi automaton.  And product_or() learned that the
    "or"-product of two Büchi automata is a Büchi automaton.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
180
181
  - spot::postprocessor has a new extra option "merge-states-min" that
    indicates above how many states twa_graph::merge_states() (which
182
    perform a very cheap pass to fuse states with identicall
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
183
    succesors) should be called before running simulation-based
184
185
    reductions.

186
187
188
189
190
191
192
  - A new function delay_branching_here(aut) can be used to simplify
    some non-deterministic branching.  If two transitions (q₁,ℓ,M,q₂)
    and (q₁,ℓ,M,q₃) differ only by their destination state, and are
    the only incoming transitions of their destination states, then q₂
    and q₃ can be merged (taking the union of their outgoing
    transitions).  This is cheap function is automatically called by
    spot::translate() after translation of a formula to GBA, before
193
194
    further simplification.  This was introduced to help with automata
    produced from formulas output by "genltl --eil-gsi" (see above).
195

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
196
197
198
199
  - spot::postprocessor has new configuration variable branch-post
    that can be used to control the use of branching-postponement
    (disabled by default) or delayed-branching (see above, enabled by
    default).  See the spot-x(7) man page for details.
200

201
202
203
204
  - spot::postprocessor is now using acd_transform() by default when
    building parity automata.  Setting option "acd=0" will revert
    to using "to_parity()" instead.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
205
206
207
  - to_parity() has been almost entirely rewritten and is a bit
    faster.

208
209
210
211
212
  - When asked to build parity automata, spot::translator is now more
    aggressively using LTL decomposition, as done in the Generic
    acceptance case before paritizing the result.  This results in
    much smaller automata in many cases.

213
214
215
  - spot::parallel_policy is an object that can be passed to some
    algorithm to specify how many threads can be used if Spot has been
    compiled with --enable-pthread.  Currently, only
216
    twa_graph::merge_states() supports it.
217

218
219
220
221
222
223
224
225
226
227
228
 Python bindings:

  - The to_str() method of automata can now export a parity game into
    the PG-Solver format by passing option 'pg'.  See
    https://spot.lrde.epita.fr/ipynb/games.html for an example.

 Deprectation notice:

  - spot::pg_print() has been deprecated in favor of spot::print_pg()
    for consistency with the rest of the API.

229
230
231
232
233
234
235
  Bugs fixed:

  - calling twa_graph::new_univ_edge(src, begin, end, cond, acc) could
    produce unexpected result if begin and end where already pointing
    into the universal edge vector, since the later can be
    reallocated during that process.

236
237
238
239
  - Printing an alternating automaton with print_dot() using 'u' to
    hide true state could produce some incorrect GraphViz output if
    the automaton as a true state as part of a universal group.

240
241
242
243
  - Due to an optimization introduces in 2.10 to parse HOA label more
    efficiently, the automaton parser could crash when parsing random
    input (not HOA) containing '[' (issue #509).

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
244
New in spot 2.10.6  (2022-05-18)
245

246
  Bugs fixed:
247
248
249

  - Fix compilation error on MacOS X.

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
253
254
255
256
257
258
259
260
  - make_twa_graph() will now preserve state number when copying a
    kripke_graph object.  As a consequence, print_dot() and
    print_hoa() will now use state numbers matching those of the
    kripke_graph (issue #505).

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
261
New in spot 2.10.5  (2022-05-03)
262

263
264
265
266
267
  Bugs fixed:

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

268
269
270
271
272
273
274
275
276
277
  - 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
278
279
    compilation on OpenBSD.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
280
281
282
  - Do not use the seq command in test cases, it is not available
    everywhere.

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

286
287
288
289
290
291
  - 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
292
New in spot 2.10.4  (2022-02-01)
293

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
294
  Bug fixed:
295
296
297
298
299
300
301

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

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

304
305
306
307
  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
308
    SCC, sbacc() could output a superfluous state.  (Issue #492)
309

310
311
312
313
314
  - 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.

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

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

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

324
  - Mealy machines resulting from SAT-based minimization could differ
325
326
327
328
    on architectures with different hash tables implementations.

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

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

331
332
333
334
  Bugs fixed:

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

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

339
340
341
  - 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
342
343
  - spot::formula::is_literal() should be const.

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
  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.
388

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

391
392
393
394
395
396
397
398
  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.

399
400
  Command-line tools:

401
402
403
404
405
406
  - 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
407
      be given and will deduce the value of the other one.
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430

    + 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
431
      sub-specifications, the controllers of which can then be glued
432
      together to satisfy the input specification.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
433
      (cf. [finkbeiner.21.nfm] in doc/spot.bib)
434
435
436

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

438
  - ltl2tgba, autfilt, dstar2tgba, and randaut learned a --buchi
439
    option, or -b for short.  This outputs Büchi automata without
440
441
442
443
444
445
446
447
448
449
450
    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.

451
452
  - autfilt learned a --kill-states=NUM[,NUM...] option.

453
454
455
456
457
458
  - 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' ...

459
  Library:
460

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
461
462
463
  - 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).
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480

  - 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.
481
482

    In addition to the previous conversion, we implemented various
483
484
485
486
487
    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,
488
    pinning, and stopping threads inside of parallel model-checking
489
    algorithms.
490

491
492
493
494
    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.
495

496
497
498
499
500
501
502
503
504
505
506
507
  - 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

508
         postprocessor::set_type(postprocessor::GeneralizedBuchi)
509
510
511

    and

512
513
         postprocessor::set_type(postprocessor::BA)

514
    by
515

516
517
518
519
520
521
522
523
524
525
         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).

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

529
  - remove_fin() learned to remove more unnecessary edges by using
530
531
    propagate_marks_vector(), both in the general case and in the
    Rabin-like case.
532

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

537
538
539
540
541
542
543
  - 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.)

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

547
548
549
550
  - 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.

551
552
553
  - print_dot() will display states from player 1 using a diamond
    shape.

554
555
556
  - print_dot() learned to display automata that correspond to Mealy
    machines specifically.

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

565
566
567
568
569
  - 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.)
570
571

      wdba-det-max   Maximum number of additional states allowed in
572
                     intermediate steps of WDBA-minimization.  If the
573
574
575
                     number of additional states reached in the
                     powerset construction or in the followup products
                     exceeds this value, WDBA-minimization is aborted.
576
                     Defaults to 4096. Set to 0 to disable.  This limit
577
578
579
                     is ignored when -D used or when det-max-states is
                     set.

580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
      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
600
601
602
603
604
605
606
607
                     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.
608

609
610
611
612
613
    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.
614

615
616
617
618
619
620
621
622
623
624
      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.)
625

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

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

638
639
640
  - twa_graph::merge_edges() had its two passes swapped.  Doing so
    improves the determinism of some automata.

641
642
643
644
  - 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
645
646
647
648
649
650
651
652
653
654
  - 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)).
655

656
657
658
659
660
661
  - 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
662
663
664
665
666
  - 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.
667

668
669
670
671
  - 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.
672
673
    Additionally, this function now returns the number of states that
    have been merged (and therefore removed from the automaton).
674

675
  - spot::zielonka_tree and spot::acd are new classes that implement the
676
677
678
679
680
    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.
681

682
683
  Python:

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

688
  - Bindings for functions related to synthesis and aig-circuits.
689
    See https://spot.lrde.epita.fr/ipynb/synthesis.html
690

691
  - spot::twa::prop_set was previously absent from the Python
692
693
694
695
    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).
696

697
698
  Bugs fixed:

699
700
  - tgba_determinize() could create parity automata using more colors
    than necessary.  (Related to issue #298)
701

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
702
703
704
705
706
  - 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.

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

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

716
717
718
719
  Documentation:

  - Mention the conda-forge package.

720
721
722
723
  Bugs fixed:

  - left->intersacting_run(right) could return a run with incorrect
    colors (likely not corresponding to any existing transition of
724
725
726
727
728
729
730
731
    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.

732

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

735
  Bugs fixed:
736

737
738
739
  - Some formulas using ->, <->, or xor were not properly detected as
    purely universal or pure eventualities.

740
741
742
  - autfilt --keep-states=... could incorrectly mention --mask-acc
    when diagnosing errors.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
743
744
  - Work around GraphViz issue 1931, causing spurious failures in the
    test suite.
745

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
746
  - Miscelaneous documentation fixes.
747

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

750
751
752
753
754
  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
755
  - Debian builds use updated standards.
756

757
758
  Bugs fixed:

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

762
763
764
765
  - On non-deterministic automata, iterated_simulations() was
    performing an (unnecessary) second iteration even when the first
    one failed to reduce the automaton.  (Issue #442)

766
767
  - When passed an incomplete automaton as input, tgba_determinize()
    would sometimes produce a complete automaton but incorrectly mark
768
769
770
771
772
773
    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.
774

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

777
778
  Bugs fixed:

779
780
781
782
  - Fix multiple spurious test suite failures on Darwin
    (Issues #426, #427, #428, #429) or when the
    Pandas package was not installed.

783
784
  - The filename python/spot/aux.py caused a problem on Windows and
    has been renamed.  Existing "import spot.aux" statements should
785
786
787
788
789
    *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
790
  - Distribution used to contain unnecessary large SVG files (Issue #422)
791

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

794
795
796
  Bugs fixed:

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

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

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

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
803
  Bug fixed:
804

805
  - Completely fix the ltlcross issue mentioned in previous release.
806

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

809
810
811
  Bugs fixed:

  - ltlcross --csv=... --product=N with N>0 could output spurious
812
    diagnostics claiming that words were rejected when evaluating
813
814
815
816
817
    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
818
New in spot 2.9.1 (2020-07-15)
819

820
821
822
823
824
825
826
  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
827
  - Option '-x wdba-minimize=N' used to accept N=0 (off), or N=1 (on).
828
829
830
831
832
833
834
835
836
837
    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
838
839
840
  - ltlsynt learned --algo=ps to use the default conversion to
    deterministic parity automata (the same as ltl2tgba -DP'max odd').

841
842
843
844
  - 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.

845
846
  Library:

847
  - product_xor() and product_xnor() are two new versions of the
848
    synchronized product.  They only work with operands that are
849
850
851
852
    deterministic automata, and build automata whose language are
    respectively the symmetric difference of the operands, and the
    complement of that.

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

859
860
861
  - remove_fin() learned a trick to remove some superfluous
    transitions.

862
863
  Bugs fixed:

864
865
  - Work around undefined behavior reported by clang 10.0.0's UBsan.

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

872
873
  - 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
874
    should simplify to Fin(1)|Fin(2)|Fin(4) after adding {1,2,4} to
875
876
877
    every place where 0 occur, and then the acceptance would be
    renumbered to Fin(0)|Fin(1)|Fin(2).  This is now fixed.

878
879
880
  - Improve ltldo diagnostics to fix spurious test-suite failure on
    systems with antique GNU libc.

881
882
883
884
885
  - 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().

886
887
888
889
890
  - 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.

891
892
893
  - 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
894
New in spot 2.9 (2020-04-30)
895

896
897
898
899
900
901
902
903
904
905
906
907
908
909
  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}"

910
  - autfilt learned the --partial-degeneralize option, to remove
911
    conjunctions of Inf, or disjunctions of Fin that appears in
912
913
    arbitrary conditions.

914
915
916
917
  - 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
918
  - When running translators, ltlcross will now display {names} when
919
920
    supplied.

921
922
923
924
  - 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.

925
926
927
928
  - 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.

929
930
931
  - ltlsynt --algo=lar uses the new version of to_parity() mentionned
    below.  The old version is available via --algo=lar.old

932
933
934
  - ltlsynt learned --csv=FILENAME, to record some statistics about
    the duration of its different phases.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
935
936
937
938
939
940
  - 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
941
942
943
944
945
946
947
948
949
  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
950
    To accommodate this, this version introduces a new operator
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
951
952
953
954
955
956
957
958
959
960
961
962
963
    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
964
    the same way, since there is no difference between X and X[!] over
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
965
966
967
968
969
970
    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.

971
972
973
974
975
976
977
978
979
980
  - 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)

981
  - partial_degeneralize() is a new function performing partial
982
983
    degeneralization to get rid of conjunctions of Inf terms, or
    disjunctions of Fin terms in acceptance conditions.
984

985
986
  - 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
987
988
989
    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
990
991
    appeared.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
992
993
994
995
996
  - 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().

997
  - propagate_marks_vector() and propagate_marks_here() are helper
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
998
    functions for propagating marks on the automaton: ignoring
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
999
1000
    self-loops and out-of-SCC transitions, marks common to all the
    input transitions of a state can be pushed to all its outgoing
For faster browsing, not all history is shown. View entire blame