Newer Older
1 2
New in spot (not yet released)

3 4 5 6 7 8
  Command-line tools:

  * ltlfilt has a new option --from-ltlf to help reducing LTLf (i.e.,
    LTL over finite words) model checking to LTL model checking.  This
    is based on a transformation by De Giacomo & Vardi (IJCAI'13).

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
9 10 11 12
  * "ltldo --stats=%R", which used to display the serial number of the
    formula processed, was renamed to "ltldo --stats=%#" to free %R
    for the following feature.

  * autfilt, dstar2tgba, ltl2tgba, ltlcross, ltldo learned to time any
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
14 15 16 17 18 19 20
    task in a more precise way thanks to %R, %[LETTER]R option. User
    or system time, for children or parent, can be measured
    separately.  A typical use-case is "ltldo --stats='... %[c]R ...'
    ..." to measure the time spent in the tool ran by ltldo, excluding
    that of ltldo.  In all tools, the difference between %r
    (wall-clock time) and %R (process time) can also be used to detect
    unreliable measurements.

22 23

24 25 26
  * from_ltlf() is a new function implementing the --from-ltlf
    transformation described above.

  * is_unambiguous() was rewritten in a more efficient way.

  * scc_info learned to determine the acceptance of simple SCCs made
30 31 32 33 34 35 36
    of a single self-loop without ressorting to remove_fin() for complex
    acceptance conditions.

  * remove_fin() has been improved to better deal with automata with
    "unclean" acceptance, i.e., acceptance sets that are declared but
    not used.  In particular, this helps scc_info to be more efficient
    at deciding the acceptance of SCCs in presence of Fin acceptance.

38 39 40 41 42
  * Simulation-based reductions now implement just bisimulations-based
    reduction on deterministic automata, to save time.  As an example,
    this halves the run time of
       genltl --rv-counter=10 | ltl2tgba

43 44 45 46 47 48 49

  * ltl2tgba was alway using the highest settings for the LTL
    simplifier, ignoring the --low and --medium options.  Now
      genltl --go-theta=12 | ltl2tgba --low --any
    is instantaneous as it should be.

50 51 52
  * Compression could encode '6' and '22' in the same way. This issue
    only appears when using the compression from intvcomp.hh.

53 54 55
  * str_sere() and str_utf8_sere() were not returning the same
    string that print_sere() and print_utf8_sere() would print.

56 57
  * Running the LTL parser in debug-mode would crash.

58 59 60 61
  * tgba_determinize() could produce incorrect deterministic automata
    when run with use_simulation (the default) on non-simplified

62 63 64 65
  * When the automaton_stream_parser reads an automaton from an
    already opened file descriptor, it will not close the file

66 67 68
  * remove_fin() could produce incorrect result on incomplete
    automata tagged as weak and deterministic.

69 70 71 72
  * calling set_acceptance() several time on an automaton could result
    in unexpected behaviors, because set_acceptance(0,...)  used to
    set the state-based acceptance flag automatically.

New in spot 2.1.2 (2016-10-14)

75 76 77 78 79 80
  Command-line tools:

  * genltl learned 5 new families of formulas
    (--tv-f1, --tv-f2, --tv-g1, --tv-g2, --tv-uu)
    defined in Tabakov & Vardi's RV'10 paper.

81 82 83 84 85 86
  * ltlcross's --csv and --json output was changed to not include
    information about the ambiguity or strength of the automata by
    default.   Computing those can be costly and not needed by
    every user, so it should now be requested explicitely using
    options --strength and --ambiguous.

87 88 89 90 91 92 93 94

  * New LTL simplification rule:

    - GF(f & q) = G(F(f) & q) if q is
      purely universal and a pure eventuality.  In particular
      GF(f & GF(g)) now ultimately simplifies to G(F(f) & F(g)).

95 96
  Bug fixes:

  * Fix spurious uninitialized read reported by valgrind when
    is_Kleene_star() is compiled by clang++.

  * Using "ltlfilt some-large-file --some-costly-filter" could take
101 102 103 104 105 106 107
    to a lot of time before displaying the first results, because the
    output of ltlfilt is buffered: the buffer had to fill up before
    being flushed.  The issue did not manifest when the input is
    standard input, because of the C++ feature that reading std::cin
    should flush std::cout; however it was well visible when reading
    from files.  Flushing is now done more regularly.

108 109 110 111
  * Fix compilation warnings when -Wimplicit-fallthrough it enabled.

  * Fix python errors on Darwin when using methods from the spot module
    inside of the spot.ltsmin submodule.

113 114
  * Fix ltlcross crash when combining --no-check with --verbose.

115 116 117
  * Adjust paths and options used in bench/dtgbasat/ to match the
    changes introduced in Spot 2.0.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
New in spot 2.1.1 (2016-09-20)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed

120 121 122
  Command-line tools:

  * ltlfilt, randltl, genltl, and ltlgrind learned to display the size
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
    (%s), Boolean size (%b), and number of atomic propositions (%a)
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
124 125
    with the --format and --output options.  A typical use-case is to
    sort formulas by size:
126 127 128 129
       genltl --dac --format='%s,%f' | sort -n | cut -d, -f2
    or to group formulas by number of atomic propositions:
       genltl --dac --output='ap-%a.ltl'

130 131 132
  * autfilt --stats learned the missing %D, %N, %P, and %W sequences,
    to complete the existing %d, %n, %p, and %w.

  * The --stats %c option of ltl2tgba, autfilt, ltldo, and dstar2tgba
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
    now accepts options to filter the SCCs to count.  For instance
135 136 137
    --stats='%[awT]c' will count the SCCs that are (a)ccepting and
    (w)eak, but (not t)erminal.  See --help for all supported filters.

138 139 140
  Bugs fixed:

  * Fix several cases where command-line tools would fail to diagnose
    write errors (e.g. when writing to a filesystem that is full).
  * Typos in genltl --help and in the man page spot-x(7).
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
New in spot 2.1 (2016-08-08)

146 147
  Command-line tools:

148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173
  * All tools that input formulas or automata (i.e., autfilt,
    dstar2tgba, ltl2tgba, ltl2tgta, ltlcross, ltldo, ltlfilt,
    ltlgrind) now have a more homogeneous handling of the default

    - If no formula/automaton have been specified, and the standard
    input is a not a tty, then the default is to read that. This is a
    change for ltl2tgba and ltl2tgta.  In particular, it simplifies

        genltl --dac | ltl2tgba -F- | autfilt ...


        genltl --dac | ltl2tgba | autfilt ...

    - If standard input is a tty and no other input has been
    specified, then an error message is printed.  This is a change for
    autfilt, dstar2tgba, ltlcross, ltldo, ltlfilt, ltlgrind, that used
    to expect the user to type formula or automata at the terminal,
    confusing people.

    - All tools now accept - as a shorthand for -F-, to force reading
    input from the standard input (regardless of whether it is a tty
    or not).  This is a change for ltl2tgba, ltl2tgta, ltlcross, and

174 175 176
  * ltldo has a new option --errors=... to specify how to deal
    with errors from executed tools.

177 178
  * ltlcross and ltldo learned to bypass the shell when executing
    simple commands (with support for single or double-quoted
179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196
    arguments, and redirection of stdin and stdout, but nothing more).

  * ltlcross and ltldo learned a new syntax to specify that an input
    formula should be written in some given syntax after rewriting
    some operators away.  For instance the defaults arguments passed
    to ltl2dstar have been changed from
         --output-format=hoa %L %O
         --output-format=hoa %[WM]L %O
    where [WM] specifies that operators W and M should be rewritten
    away.  As a consequence running
         ltldo ltl2dstar -f 'a M b'
    will now work and call ltl2dstar on the equivalent formula
    'b U (a & b)' instead.  The operators that can be listed between
    brackets are the same as those of ltlfilt --unabbreviate option.

  * ltlcross learned to show some counterexamples when diagnosing
    failures of cross-comparison checks against random state spaces.

198 199
  * autfilt learned to filter automata by count of SCCs (--sccs=RANGE)
    or by type of SCCs (--accepting-sccs=RANGE,
200 201 202
    --rejecting-sccs=RANGE, trivial-sccs=RANGE, --terminal-sccs=RANGE,
    --weak-sccs=RANGE, --inherently-weak-sccs=RANGE).

  * autfilt learned --remove-unused-ap to remove atomic propositions
204 205
    that are declared in the input automaton, but not actually used.
    This of course makes sense only for input/output formats that
    declare atomic propositions (HOA & DSTAR).

  * autfilt learned two options to filter automata by count of used or
209 210 211 212
    unused atomic propositions: --used-ap=RANGE --unused-ap=RANGE.
    These differ from --ap=RANGE that only consider *declared* atomic
    propositions, regardless of whether they are actually used.

213 214
  * autfilt learned to filter automata by count of nondeterministsic
    states with --nondet-states=RANGE.

  * autfilt learned to filter automata representing stutter-invariant
217 218
    properties with --is-stutter-invariant.

  * autfilt learned two new options to highlight non-determinism:
    --highlight-nondet-states=NUM and --highlight-nondet-states=NUM
221 222
    where NUM is a color number.  Additionally --highlight-nondet=NUM is
    a shorthand for using the two.

  * autfilt learned to highlight a run matching a given word using the
225 226 227
    --highlight-word=[NUM,]WORD option.  However currently this only
    work on automata with Fin-less acceptance.

228 229 230
  * autfilt learned two options --generalized-rabin and
    --generalized-streett to convert the acceptance conditions.

  * genltl learned three new families: --dac-patterns=1..45,
232 233 234
    --eh-patterns=1..12, and --sb-patterns=1..27.  Unlike other options
    these do not output scalable patterns, but simply a list of formulas
    appearing in these three papers: Dwyer et al (FMSP'98), Etessami &
    Holzmann (Concur'00), Somenzi & Bloem (CAV'00).

237 238
  * genltl learned two options, --positive and --negative, to control
    wether formulas should be output after negation or not (or both).

240 241 242 243 244 245 246 247 248 249 250 251 252
  * The formater used by --format (for ltlfilt, ltlgrind, genltl,
    randltl) or --stats (for autfilt, dstar2tgba, ltl2tgba, ltldo,
    randaut) learned to recognize double-quoted fields and double the
    double-quotes output inbetween as expected from RFC4180-compliant
    CSV files.  For instance
      ltl2tgba -f 'a U "b+c"' --stats='"%f",%s'
    will output
      "a U ""b+c""",2

  * The --csv-escape option of genltl, ltlfilt, ltlgrind, and randltl
    is now deprecated.  The option is still here, but hidden and

253 254
  * The --stats option of autfilt, dstar2tgba, ltl2tgba, ltldo,
    randaut learned to display the output (or input if that makes
    sense) automaton as a HOA one-liner using %h (or %H), helping to
256 257
    create CSV files contained automata.

258 259 260 261
  * autfilt and dstar2tgba learned to read automata from columns in
    CSV files, specified using the same filename/COLUMN syntax used by
    tools reading formulas.

262 263 264
  * Arguments passed to -x (in ltl2tgba, ltl2tgta, autfilt, dstar2tgba)
    that are not used are now reported as they might be typos.
    This ocurred a couple of times in our test-suite.  A similar
    check is done for the arguments of autfilt --sat-minimize=...

267 268 269 270 271 272 273 274 275

  * The print_hoa() function will now output version 1.1 of the HOA
    format when passed the "1.1" option (i.e., use -H1.1 from any
    command-line tool).  As far as Spot is concerned, this allows
    negated properties to be expressed.  Version 1 of the HOA format
    is still the default, but we plan to default to version 1.1 in the

276 277 278 279 280 281 282
  * The "highlight-states" and "highlight-edges" named properties,
    which were introduced in 1.99.8, will now be output using
    "spot.highlight.edges:" and "spot.highlight.states:" headers if
    version 1.1 of the HOA format is selected.  The automaton parser
    was secretly able of reading that since 1.99.8, but that is now
    documented at

283 284 285
  * highlight_nondet_states() and highlight_nondet_edges() are
    new functions that define the above two named properties.

  * is_deterministic(), is_terminal(), is_weak(), and
287 288 289
    is_inherently_weak(), count_nondet_states(),
    highlight_nondet_edges(), highlight_nondet_states() will update
    the corresponding properties of the automaton as a side-effect of
    their check.

292 293 294 295 296 297
  * the sbacc() function, used by "ltl2tgba -S" and "autfilt -S" to
    convert automata to state-based acceptance, learned some tricks
    (using SCCs, pulling accepting marks common to all outgoing edges,
    and pushing acceptance marks common to all incoming edges) to
    reduce the number of additional states needed.

298 299 300 301
  * to_generalized_rabin() and to_generalized_streett() are two new
    functions that convert the acceptance condition as requested
    without changing the transition structure.

302 303 304
  * language_containment_checker now has default values for all
    parameters of its constructor.

305 306 307 308
  * spot::twa_run has a new method, project(), that can be used to
    project a run found in a product onto one of the original operand.
    This is for instance used by autfilt --highlight-word.

309 310 311 312
    The old spot::project_twa_run() function has been removed: it was
    not used anywhere in Spot, and had an obvious bug in its
    implementation, so it cannot be missed by anyone.

313 314
  * spot::twa has two new methods that supplement is_empty():
    twa::accepting_run() and twa::accepting_word().  They compute
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
    what their names suggest.  Note that twa::accepting_run(), unlike
316 317 318
    the two others, is currently restricted to automata with Fin-less

319 320 321 322 323
  * spot::check_stutter_invariance() can now work on non-deterministic
    automata for which no corresponding formula is known.  This
    implies that "autfilt --check=stutter" will now label all
    automata, not just deterministic automata.

  * New LTL and PSL simplification rules:
325 326
    - if e is pure eventuality and g => e, then e U g = Fg
    - if u is purely universal and u => g, then u R g = Gg
327 328
    - {s[*0..j]}[]->b = {s[*1..j]}[]->b
    - {s[*0..j]}<>->b = {s[*1..j]}<>->b

330 331 332 333
  * spot::twa::succ_iterable renamed to
    spot::internal::twa_succ_iterable to make it clear this is not for
    public consumption.

334 335 336 337 338
  * spot::fair_kripke::state_acceptance_conditions() renamed to
    spot::fair_kripke::state_acceptance_mark() for consistency.  This
    is backward incompatible, but we are not aware of any actual use
    of this method.

339 340

  * The __format__() method for formula supports the same
342 343 344 345
    operator-rewritting feature introduced in ltldo and ltlcross.
    So "{:[i]s}".format(f) is the same as

346 347
  * Bindings for language_containment_checker were added.

348 349
  * Bindings for randomize() were added.

350 351 352
  * Iterating over edges via "aut.out(s)" or "aut.edges()"
    now allows modifying the edge fields.

  * Under IPython the spot.ltsmin module now offers a
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
    %%pml magic to define promela models, compile them
355 356 357
    with spins, and dynamically load them.   This is
    akin to the %%dve magic that was already supported.

358 359 360 361
  * The %%dve and %%pml magics honor the SPOT_TMPDIR and
    TMPDIR environment variables.  This especially helps
    when the current directory is read-only.

362 363 364 365

  * A new example page shows how to test the equivalence of
    two LTL/PSL formulas.

367 368
  * A new page discusses explicit vs. on-the-fly interfaces for
    exploring automata in C++.

  * Another new page shows how to implement an on-the-fly Kripke
    structure for a custom state space.
372 373

374 375
  * The concepts.html page now lists all named properties
    used by automata.

377 378 379 380 381 382
  Bug fixes:

  * When ltlcross found a bug using a product of complemented
    automata, the error message would report "Comp(Ni)*Comp(Pj)" as
    non-empty while the actual culprit was "Comp(Nj)*Comp(Pi)".

383 384 385
  * Fix some non-deterministic execution of minimize_wdba(), causing
    test-suite failures with the future G++ 7, and clang 3.9.

386 387 388
  * print_lbtt() had a memory leak when printing states without

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
New in spot 2.0.3 (2016-07-11)

391 392 393 394 395
  Bug fixes:

  * The degen-lcache=1 option of the degeneralization algorithm (which
    is a default option) did not behave exactly as documented: instead
    of reusing the first level ever created for a state where the
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
396 397
    choice of the level is free, it reused the last level ever used.
    This caused some posterior simulation-based reductions to be less
    efficient at reducing automata (on the average).
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
  * The generalized testing automata displayed by the online
    translator were incorrect (those output by ltl2tgta were OK).
  * ltl2tgta should not offer options --ba, --monitor, --tgba and such.
  * the relabel() function could incorrectly unregister old atomic
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
403 404 405
    propositions even when they were still used in the output (e.g.,
    if a&p0 is relabeled to p0&p1).  This could cause ltldo and the
    online translator to report errors.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
407 408 409 410 411 412 413 414
New in spot 2.0.2 (2016-06-17)


  * We now have a citing page at
    providing a list of references about Spot.
  * The Python examples have been augmented with the two examples
    from our ATVA'16 tool paper.

416 417 418 419
  Bug fixes:

  * Fix compilation error observed with Clang++ 3.7.1 and GCC 6.1.1
  * Fix an infinite recursion in relabel_bse().
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
  * Various small typos and cosmetic cleanups.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
New in spot 2.0.1 (2016-05-09)

425 426

  * twa::unregister_ap() and twa_graph::remove_unused_ap() are new
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
    methods introduced to fix some of the bugs listed below.

430 431 432 433 434

  * Add missing documentation for the option string passed to

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
  * There is now a spot(7) man page listing all installed
436 437
    command-line tools.

438 439 440 441

  * The tgba_determinize() function is now accessible in Python.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
442 443
  Bug fixes:

  * The automaton parser would choke on comments like /******/.
  * check_strength() should also set negated properties.
446 447 448
  * Fix autfilt to apply --simplify-exclusive-ap only after
    the simplifications of (--small/--deterministic) have
    been performed.
449 450
  * The automaton parser did not fully register atomic propositions
    for automata read from never claim or as LBTT.
  * spot::ltsmin::kripke() had the same issue.
452 453 454 455
  * The sub_stats_reachable() function used to count the number
    of transitions based on the number of atomic propositions
    actually *used* by the automaton instead of using the number
    of AP declared.
456 457 458 459 460
  * print_hoa() will now output all the atomic propositions that have
    been registered, not only those that are used in the automaton.
    (Note that it will also throw an exception if the automaton uses
    an unregistered AP; this is how some of the above bugs were
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
  * For Small or Deterministic preference, the postprocessor
462 463 464
    will now unregister atomic propositions that are no longer
    used in labels.   Simplification of exclusive properties
    and remove_ap::strip() will do similarly.
465 466
  * bench/ltl2tgba/ was not working since the source code
    reorganization of 1.99.7.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
  * Various typos and minor documentation fixes.


Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
New in spot 2.0 (2016-04-11)

472 473 474
  Command-line tools:

  * ltlfilt now also support the --accept-word=WORD and
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
475 476
    --reject-word=WORD options that were introduced in autfilt in the
    previous version.

478 479 480

  * The output of spot.atomic_prop_collect() is printable and
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
    can now be passed directly to spot.ltsmin.model.kripke().

483 484 485 486

  * digraph::valid_trans() renamed to digraph::is_valid_edge().

487 488

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
489 490 491 492 493
  * The concepts page ( now
    includes a highlevel description of the architecture, and some
    notes aboute automata properties.

  * More Doxygen documentation for spot::formula and spot::digraph.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
New in spot 1.99.9 (2016-03-14)

497 498
  Command-line tools:

499 500 501
  * autfilt has two new options: --accept-word=WORD and
    --reject-word=WORD for filtering automata that accept or reject
    some word.  The option may be used multiple times.

503 504

505 506 507
  * The parse_word() function can be used to parse a lasso-shaped
    word and build a twa_word.  The twa_word::as_automaton()
    method can be used to create an automaton out of that.
  * twa::ap_var() renamed to twa::ap_vars().
509 510 511 512
  * emptiness_check_instantiator::min_acceptance_conditions() and
    emptiness_check_instantiator::max_acceptance_conditions() renamed
    to emptiness_check_instantiator::min_sets() and
513 514
  * tgba_reachable_iterator (and subclasses) was renamed to
    twa_reachable_iterator for consistency.

516 517 518 519

  * The page should help
    people migrating old C++ code written for Spot 1.2.x, and update
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
    it for (the upcoming) Spot 2.0.

522 523 524 525
  Bug fixes:

  * spot/twaalgos/gtec/gtec.hh was incorrectly installed as
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
  * The shared libraries should now compile again on Darwin.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
New in spot 1.99.8 (2016-02-18)

530 531
  Command-line tools:

532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558
  * ltl2tgba now also support the --generic option (already supported
    by ltldo and autfilt) to lift any restriction on the acceptance
    condition produced.  This option now has a short version: -G.

  * ltl2tgba and autfilt have learnt how to determinize automata.
    For this to work, --generic acceptance should be enabled (this
    is the default for autfilt, but not for ltl2tgba).

    "ltl2tgba -G -D" will now always outpout a deterministic automaton.
    It can be an automaton with transition-based parity acceptance in
    case Spot could not find a deterministic automaton with (maybe
    generalized) Büchi acceptance.

    "ltl2tgba -D" is unchanged (the --tgba acceptance is the default),
    and will output a deterministic automaton with (generalized) Büchi
    acceptance only if one could be found.  Otherwise a
    non-deterministic automaton is output, but this does NOT mean that
    no deterministic Büchi automaton exist for this formula.  It only
    means Spot could not find it.

    "autfilt -D" will determinize any automaton, because --generic
    acceptance is the default for autfilt.

    "autfilt -D --tgba" will behave like "ltl2tgba -D", i.e., it may
    fail to find a deterministic automaton (even if one exists) and
    return a nondeterministic automaton.

559 560 561 562 563
  * "autfilt --complement" now also works for non-deterministic
    automata but will output a deterministic automaton.
    "autfilt --complement --tgba" will likely output a
    nondeterministic TGBA.

564 565 566
  * autfilt has a new option, --included-in, to filter automata whose
    language are included in the language of a given automaton.

567 568 569
  * autfilt has a new option, --equivalent-to, to filter automata
    that are equivalent (language-wise) to a given automaton.

570 571 572 573 574 575 576
  * ltlcross has a new option --determinize to instruct it to
    complement non-deterministic automata via determinization.  This
    option is not enabled by default as it can potentially be slow and
    generate large automata.  When --determinize is given, option
    --product=0 is implied, since the tests based on products with
    random state-space are pointless for deterministic automata.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
577 578 579
  * ltl2tgba and ltldo now support %< and %> in the string passed
    to --stats when reading formulas from a CSV file.

580 581 582 583 584
  * ltlfilt's option --size-min=N, --size-max=N, --bsize-min=N, and
    --bsize-max=N have been reimplemented as --size=RANGE and
    --bsize=RANGE.  The old names are still supported for backward
    compatibility, but they are not documented anymore.

585 586
  * ltlfilt's option --ap=N can now take a RANGE as parameter.

587 588 589
  * autfilt now has a --ap=RANGE option to filter automata by number
    of atomic propositions.

590 591 592 593 594

  * Building products with different dictionaries now raise an
    exception instead of using an assertion that could be disabled.

  * The load_ltsmin() function has been split in two.  Now you should
    first call ltsmin_model::load(filename) to create an ltsmin_model,
    and then call the ltsmin_model::kripke(...) method to create an
598 599 600
    automaton that can be iterated on the fly.  The intermediate
    object can be queried about the supported variables and their

602 603 604 605 606 607 608 609 610 611 612 613
  * print_dot() now accepts several new options:
    - use "<N" to specify a maximum number of states to output.
      Incomplete states are then marked appropriately.  For a quick
      example, compare
	ltl2tgba -D 'Ga | Gb | Gc' -d'<3'
        ltl2tgba -D 'Ga | Gb | Gc' -d
    - use "C(color)" to specify the color to use for filling states.
    - use "#" to display the internal number of each transition
    - use "k" to use state-based labels when possible.  This is
      similar to the "k" option already supported by print_hoa(), and
      is useful when printing Kripke structures.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
615 616
  * Option "k" is automatically used by print_dot() and print_hoa()
    when printing Kripke structures.

618 619 620 621
  * print_dot() also honnor two new automaton properties called
    "highlight-edges" and "highlight-states".  These are used to color
    a subset of edges or transitions.

622 623 624 625
  * There is a new tgba_determinize() function.  Despite its name, it
    in facts works on transition-based Büchi automaton, and will first
    degeneralize any automaton with generalized Büchi acceptance.

626 627 628
  * The twa_safra_complement class has been removed.  Use
    tgba_determinize() and dtwa_complement() instead.

629 630
  * The twa::transition_annotation() and
    twa::compute_support_conditions() methods have been removed.

632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657
  * The interface for all functions parsing formulas (LTL, PSL, SERE,
    etc.) has been changed to use an interface similar to the one used
    for parsing automata.  These function now return a parsed_formula
    object that includes both a formula and a list of syntax errors.

    Typically a function written as

       spot::formula read(std::string input)
	  spot::parse_error_list pel;
	  spot::formula f = spot::parse_infix_psl(input, pel);
	  if (spot::format_parse_errors(std::cerr, input, pel))
	  return f;

    should be updated to

       spot::formula read(std::string input)
	  spot::parsed_formula pf = spot::parse_infix_psl(input);
	  if (pf.format_errors(std::cerr))
	  return pf.f;

658 659

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
660 661 662
  * The ltsmin interface has been binded in Python.  It also
    comes with a %%dve cell magic to edit DiVinE models in the notebook.
    See for a short example.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
664 665 666 667 668
  * spot.setup() sets de maximum number of states to display in
    automata to 50 by default, as more states is likely to be
    unreadable (and slow to process by GraphViz).  This can be
    overridden by calling spot.setup(max_states=N).

669 670 671 672
  * Automata now have methods to color selected states and
    transitions.  See for an example.

673 674 675 676 677

  * There is a new page giving informal illustrations (and extra
    pointers) for some concepts used in Spot.

  Bug fixes:
680 681 682

  * Using ltl2tgba -U would fail to output the unambiguous property
    (regression introduced in 1.99.7)
683 684
  * ltlfilt, autfilt, randltl, and randaut could easily crash when
    compiled statically (i.e., with configure --disable-shared).
  * "1 U (a | Fb)" was not always simplified to "F(a | b)".
686 687
  * destroying the operands of an otf_product() before the product
    itself could crash.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
New in spot 1.99.7 (2016-01-15)
690 691 692

  Command-line tools:

  * BACKWARD INCOMPATIBLE CHANGE: All tools that output automata now
    use the HOA format by default instead of the GraphViz output.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
    This makes it easier to pipe several commands together.
696 697 698 699 700 701

    If you have an old script that relies on GraphViz being the default
    output and that you do not want to update it, use
       export SPOT_DEFAULT_FORMAT=dot
    to get the old behavior back.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
702 703 704
  * Tools that output automata now accept -d as a shorthand for --dot
    since requesting the GraphViz (a.k.a. dot) output by hand is now
    more frequent.
705 706
    randaut's short option for specifying edge-density used to be -d:
    it has been renamed to -e.

  * The SPOT_DEFAULT_FORMAT environment variable can be set to 'dot'
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
709 710
    or 'hoa' to force a default output format for automata.  Additional
    options may also be added, as in SPOT_DEFAULT_FORMAT='hoa=iv'.

712 713
  * autfilt has a new option: --is-inherently-weak.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
714 715 716
  * The --check=strength option of all tools that produce automata
    will also test if an automaton is inherently weak.

717 718

719 720 721 722 723 724 725 726 727
  * Installed headers now assume that they will be included as
    #include <spot/subdir/header.hh>
    instead of
    #include <subdir/header.hh>

    This implies that when Spot headers are installed in
    /usr/include/spot/... (the default when using the Debian packages)
    or /usr/local/include/spot/... (the default when compiling from
    source), then it is no longuer necessary to add
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
728 729 730
    -I/usr/include/spot or -I/usr/local/include/spot when compiling,
    as /usr/include and /usr/local/include are usually searched by
731 732 733 734

    Inside the source distribution, the subdirectory src/ has been
    renamed to spot/, so that the root of the source tree can also be
    put on the preprocessor's search path to compile against a
735 736
    non-installed version of Spot.  Similarly, iface/ltsmin/ has been
    renamed to spot/ltsmin/, so that installed and non-installed
    directories can be used similarly.

739 740 741 742
  * twa::~twa() is now calling
    so this does not need to be done in any subclass.

743 744 745 746
  * is_inherently_weak_automaton() is a new function, and
    check_strength() has been modified to also check inherently weak

747 748 749 750
  * decompose_strength() is now extracting inherently weak SCCs
    instead of just weak SCCs.  This gets rid of some corner cases
    that used to require ad hoc handling.

751 752 753 754
  * acc_cond::acc_code's methods append_or(), append_and(), and
    shift_left() have been replaced by operators |=, &=, <<=, and for
    completeness the operators |, &, and << have been added.

755 756 757
  * Several methods have been removed from the acc_cond
    class because they were simply redundant with the methods of
    acc_cond::mark_t, and more complex to use.

       acc_cond::marks(...)      -> use acc_cond::mark_t(...)
       acc_cond::sets(m)         -> use m.sets()
       acc_cond::has(m, u)       -> use m.has(u)
762 763 764 765
       acc_cond::cup(l, r)       -> use l | r
       acc_cond::cap(l, r)       -> use l & r
       acc_cond::set_minus(l, r) -> use l - r

    Additionally, the following methods/functions have been renamed:
767 768 769

       acc_cond::is_tt() -> acc_cond::is_t()
       acc_cond::is_ff() -> acc_cond::is_f()
       parse_acc_code()  -> acc_cond::acc_code(...)

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
  * Automata property flags (those that tell whether the automaton is
773 774 775
    deterministic, weak, stutter-invariant, etc.) are now stored using
    three-valued logic: in addition to "maybe"/"yes" they can now also
    represent "no".  This is some preparation for the upcomming
776 777 778 779 780 781 782 783
    support of the HOA v1.1 format, but it also saves time in some
    algorithms (e.g, is_deterministic() can now return immediately on
    automata marked as not deterministic).

  * The automaton parser now accept negated properties as they will be
    introduced in HOA v1.1, and will check for some inconsistencies.
    These properties are stored and used when appropriate, but they
    are not yet output by the HOA printer.

785 786

787 788 789 790
  * Iterating over the transitions leaving a state (the
    twa_graph::out() C++ function) is now possible in Python.  See for a demonstration.

791 792 793 794
  * Membership to acceptance sets can be specified using Python list
    when calling for instance the Python version of twa_graph::new_edge().
    See for a demonstration.

795 796 797
  * Automaton states can be named via the set_state_names() method.
    See for an example.

798 799 800 801 802

  * There is a new page explaining how to compile example programs and
    and link them with Spot.

803 804 805 806 807
  * Python bindings for manipulating acceptance conditions are
    demonstrated by,
    and a Python implementation of the product of two automata is
    illustrated by

808 809 810 811 812 813 814 815 816 817 818 819
  Source code reorganisation:

  * A lot of directories have been shuffled around in the
      src/                   ->  spot/    (see rational above)
      iface/ltsmin/  (code)  ->  spot/ltsmin/
      wrap/python/           ->  python/
      src/tests/             ->  tests/core/
      src/sanity/            ->  tests/sanity/
      iface/ltsmin/  (tests) ->  tests/ltsmin/
      wrap/python/tests      ->  tests/python/

820 821
  Bug fixes:

822 823
  * twa_graph would incorrectly replace named-states during
    purge_dead_states and purge_unreachable_states.
824 825
  * twa::ap() would contain duplicates when an atomic proposition
    was registered several times.
826 827
  * product() would incorrectly mark the product of two
    sttuter-sensitive automata as stutter-sensitive as well.
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
828 829
  * complete() could incorrectly reuse an existing (but accepting!)
    state as a sink.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
New in spot 1.99.6 (2015-12-04)

833 834
  Command-line tools:

835 836 837 838
  * autfilt has two new filters: --is-weak and --is-terminal.

  * autfilt has a new transformation: --decompose-strength,
    implementing the decomposition of our TACAS'13 paper.
839 840
    A demonstration of this feature via the Python bindings
    can be found at

842 843 844 845 846 847
  * All tools that output HOA files accept a --check=strength option
    to request automata to be marked as "weak" or "terminal" as
    appropriate.  Without this option, these properties may only be
    set as a side-effect of running transformations that use this

848 849 850 851 852 853 854

  * Properties of automata (like the "properties:" line of the HOA
    format) are stored as bits whose interpretation is True=yes,
    False=maybe.  Having getters like "aut->is_deterministic()" or
    "aut->is_unambiguous()" was confusing, because there are separate
    functions "is_deterministic(aut)" and "is_unambiguous(aut)" that
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
855 856
    do actually check the automaton.  The getters have been renamed to
    avoid confusion, and get names more in line with the HOA format.
857 858 859 860 861 862 863 864 865

    - twa::has_state_based_acc() -> twa::prop_state_acc()
    - twa::prop_state_based_acc(bool) -> twa::prop_state_acc(bool)
    - twa::is_inherently_weak() -> twa::prop_inherently_weak()
    - twa::is_deterministic() -> twa::prop_deterministic()
    - twa::is_unambiguous() -> twa::prop_unambiguous()
    - twa::is_stutter_invariant() -> twa::prop_stutter_invariant()
    - twa::is_stutter_sensitive() -> twa::prop_stutter_sensitive()

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
    The setters have the same names as the getters, except they take a
867 868 869
    Boolean argument.  This argument used to be optionnal (defaulting
    to True), but it no longer is.

870 871 872 873 874 875 876 877 878 879
  * Automata now support the "weak" and "terminal" properties in
    addition to the previously supported "inherently-weak".

  * By default the HOA printer tries not to bloat the output with
    properties that are redundant and probably useless.  The HOA
    printer now has a new option "v" (use "-Hv" from the command line)
    to output more verbose "properties:".  This currently includes
    outputing "no-univ-branch", outputting "unambiguous" even for
    automata already tagged as "deterministic", and "inherently-weak"
    or "weak" even for automata tagged "weak" or "terminal".

881 882 883 884
  * The HOA printer has a new option "k" (use "-Hk" from the command
    line) to output automata using state labels whenever possible.
    This is useful to print Kripke structures.

885 886 887 888 889
  * The dot output will display pair of states when displaying an
    automaton built as an explicit product.  This works in IPython
    with spot.product() or spot.product_or() and in the shell with
    autfilt's --product or --product-or options.

890 891 892 893 894 895 896
  * The print_dot() function supports a new option, +N, where N is a
    positive integer that will be added to all set numbers in the
    output.  This is convenient when displaying two automata before
    building their product: use +N to shift the displayed sets of the
    second automaton by the number of acceptance sets N of the first

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
  * The sat minimization for DTωA now does a better job at selecting
898 899 900 901 902
    reference automata when the output acceptance is the the same as
    the input acceptance.  This can provide nice speedups when tring
    to syntethise larged automata with different acceptance

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
  * Explicit Kripke structures (i.e., stored as explicit graphs) have
    been rewritten above the graph class, using an interface similar
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
905 906
    to the twa class.  The new class is called kripke_graph.  The ad
    hoc Kripke parser and printer have been removed, because we can
907 908
    now use print_hoa() with the "k" option to print Kripke structure
    in the HOA format, and furthermore the parse_aut() function now
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
    has an option to load such an HOA file as a kripke_graph.

911 912 913 914
  * The HOA parser now accepts identifier, aliases, and headernames
    containing dots, as this will be allowed in the next version of
    the HOA format.

915 916
  * Renamings:
    is_guarantee_automaton() -> is_terminal_automaton()
    tgba_run -> twa_run
    twa_word::print -> operator<<
919 920
    dtgba_sat_synthetize() -> dtwa_sat_synthetize()
    dtgba_sat_synthetize_dichotomy() -> dtwa_sat_synthetize_dichotomy()

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed

  * Add bindings for is_unambiguous().
  * Better interface for sat_minimize().

  Bug fixes:
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed

  * the HOA parser was ignoring the "unambiguous" property.
930 931
  * --dot=Bb should work like --dot=b, allowing us to disable
    a B option set via an environment variable.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
New in spot 1.99.5 (2015-11-03)

935 936 937
  Command-line tools:

  * autfilt has gained a --complement option.
    It currently works only for deterministic automata.

  * By default, autfilt does not simplify automata (this has not
    changed), as if the --low --any options were used.  But now, if
942 943 944
    one of --small, --deterministic, or --any is given, the
    optimization level automatically defaults to --high (unless
    specified otherwise).  For symmetry, if one of --low, --medium, or
    --high is given, then the translation intent defaults to --small
946 947
    (unless specified otherwise).

948 949 950 951
  * autfilt, dstar2tgba, ltlcross, and ltldo now trust the (supported)
    automaton properties declared in any HOA file they read.  This can
    be disabled with option --trust-hoa=no.

952 953 954
  * ltlgrind FILENAME[/COL] is now the same as
    ltlgrind -F FILENAME[/COL] for consistency with ltlfilt.

955 956

957 958 959 960 961
  * dtgba_complement() was renamed to dtwa_complement(), moved to
    complement.hh, and its purpose was restricted to just completing
    the automaton and complementing its acceptance condition.  Any
    further acceptance condition transformation can be done with
    to_generalized_buchi() or remove_fin().
962 963 964 965 966

  * The remove_fin() has learnt how to better deal with automata that
    are declared as weak.  This code was previously in

967 968 969 970 971
  * scc_filter_states() has learnt to remove useless acceptance marks
    that are on transitions between SCCs, while preserving state-based
    acceptance.  The most visible effect is in the output of "ltl2tgba
    -s XXXa": it used to have 5 accepting states, it now has only one.
    (Changing removing acceptance of those 4 states has no effect on
    the language, but it speeds up some algorithms like NDFS-based
973 974
    emptiness checks, as discussed in our Spin'15 paper.)

975 976 977
  * The HOA parser will diagnose any version that is not v1, unless it
    looks like a subversion of v1 and no parse error was detected.

  * The way to pass option to the automaton parser has been changed to
    make it easier to introduce new options.  One such new option is
980 981
    "trust_hoa": when true (the default) supported properties declared
    in HOA files are trusted even if they cannot be easily be verified.
982 983 984 985 986
    Another option "raise_errors" now replaces the method

  * The output of the automaton parser now include the list of parse
    errors (that does not have to be passed as a parameters) and the
Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
    input filename (making the output of error messages easier).

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
  * The following renamings make the code more consistent:
990 991 992
    ltl_simplifier -> tl_simplifier
    tgba_statistics::transitions -> twa_statistics::edges
    tgba_sub_statistics::sub_transitions -> twa_sub_statistics::transitions
    tgba_run -> twa_run
    reduce_run -> twa_run::reduce
995 996 997 998
    replay_tgba_run -> twa_run::replay
    print_tgba_run -> operator<<
    tgba_run_to_tgba -> twa_run::as_twa
    format_parse_aut_errors -> parsed_aut::format_errors
999 1000 1001 1002 1003 1004
    twa_succ_iterator::current_state -> twa_succ_iterator::dst
    twa_succ_iterator::current_condition -> twa_succ_iterator::cond
    twa_succ_iterator::current_acceptance_conditions -> twa_succ_iterator::acc
    ta_succ_iterator::current_state -> ta_succ_iterator::dst
    ta_succ_iterator::current_condition -> ta_succ_iterator::cond
    ta_succ_iterator::current_acceptance_conditions -> ta_succ_iterator::acc

1006 1007

  * The minimum supported Python version is now 3.3.
  * Add bindings for complete() and dtwa_complement()
1010 1011
  * Formulas now have a custom __format__ function.  See for examples.
1012 1013
  * The Debian package is now compiled for all Python3 versions
    supported by Debian, not just the default one.
  * Automata now have get_name()/set_name() methods.
1015 1016 1017
  * spot.postprocess(aut, *options), or aut.postprocess(*options)
    simplify the use of the spot.postprocessor object.  (Just like we
    have spot.translate() on top of spot.translator().)
1018 1019 1020 1021 1022 1023 1024 1025
  * spot.automata() and spot.automaton() now have additional
    optional arguments:
    - timeout: to restrict the runtime of commands that
      produce automata
    - trust_hoa: can be set to False to ignore HOA properties
      that cannot be easily verified
    - ignore_abort: can be set to False if you do not want to
      skip automata ended with --ABORT--.

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
1027 1028 1029 1030 1031 1032

  * There is a new page showing how to use spot::postprocessor
    to convert any type of automaton to Büchi.

1033 1034
  Bugs fixed:

  * Work around some weird exception raised when using the
1036 1037 1038 1039 1040
    randltlgenerator under Python 3.5.
  * Recognize "nullptr" formulas as None in Python.
  * Fix compilation of bench/stutter/
  * Handle saturation of formula reference counts.
  * Fix typo in the Python code for the CGI server.
  * "randaut -Q0 1" used to segfault.
1042 1043
  * "ltlgrind -F FILENAME/COL" did not preserve other CSV columns.
  * "ltlgrind --help" did not document FORMAT.
  * unabbreviate could easily use forbidden operators.
1045 1046
  * "autfilt --is-unambiguous" could fail to detect the nonambiguity
    of some automata with empty languages.
1047 1048 1049
  * When parsing long tokens (e.g, state labels representing
    very large strings) the automaton parser could die with
    "input buffer overflow, can't enlarge buffer because scanner uses REJECT"

Alexandre Duret-Lutz's avatar
Alexandre Duret-Lutz committed
New in spot 1.99.4 (2015-10-01)

1053 1054
  New features:

1055 1056 1057 1058
  * autfilt's --sat-minimize now takes a "colored" option to constrain
    all transitions (or states) in the output automaton to belong to
    exactly one acceptance sets.  This is useful when targeting parity

1060 1061 1062 1063 1064 1065 1066 1067 1068 1069
  * autfilt has a new --product-or option.  This builds a synchronized
    product of two (completed of needed) automata in order to
    recognize the *sum* of their languages.  This works by just using
    the disjunction of their acceptance conditions (with appropriate
    renumbering of the acceptance sets).

    For consistency, the --product option (that builds a synchronized
    product that recognizes the *intersection* of the languages) now
    also has a --product-and alias.

1070 1071 1072 1073 1074 1075 1076 1077 1078 1079
  * the parser for ltl2dstar's format has been merged with the parser
    for the other automata formats.  This implies two things:
    - autfilt and dstar2tgba (despite its name) can now both read
      automata written in any of the four supported syntaxes
      (ltl2dstar's, lbtt's, HOA, never claim).
    - "dstar2tgba some files..." now behaves exactly like
      "autfilt --tgba --high --small some files...".
      (But dstar2tgba does not offer all the filtering and
      transformations options of autfilt.)

1080 1081
  Major code changes and reorganization: