1New in spot 2.10.2 (2021-12-03) 2 3 Bugs fixed: 4 5 - twa_graph::purge_dead_states() now also removes edges labeled by 6 bddfalse. 7 8 - only use sched_getcpu() and pthread_setaffinity_np() when they are 9 available. 10 11 - Using ##300 in a SERE will report that the repeatition exceeds the 12 allowed value using a parse error, not as an exception. 13 14 - spot::formula::is_literal() should be const. 15 16New in spot 2.10.1 (2021-11-19) 17 18 Build: 19 20 - Python 3.5 or later is now required (unless Python bindings are 21 disabled). Python 3.5 reached end-of-life one year ago, so we 22 believe support for older versions of Python will not be missed. 23 24 Library: 25 26 - The sbacc() function now defines the "original-states" property, 27 allowing to map an output state back to its input. 28 29 Bugs fixed: 30 31 - Ranged repetition operators from LTL/PSL, like [*a..b], 32 [->a..b] or even F[a..b] used to store and handle a and b 33 as 8-bit values without overflow checks. So for instance 34 {a[*260];b} was silently interpreted as {a[*4];b} 35 This version still restricts those bounds to 8 bits, but now 36 diagnose overflow checks while parsing and constructing formulas. 37 Also the so called "trivial simplification rules" will not be 38 applied in case they would lead to an overflow. For instance 39 {a;[*150];[*50];b} is rewritten to {a;[*200];b} 40 but 41 {a;[*150];[*150];b} is untouched. 42 43 - Fix a compilation error on system with glibc older than 2.18, 44 where <inttypes.h> does not define some C99 macro by default when 45 compiled in C++ mode. (Such old libraries are used when compiling 46 packages for conda-forge, which use CentOS 6 as building environment.) 47 48 - Fix a link error of tests/ltsmin/modelcheck not finding BDD functions 49 on some systems (observed on CentOS 6 again). 50 51 - Fix spurious test-suite failures under newer Jupyter 52 installations. IPykernel 6.0 now captures stdout/stderr from 53 subprocesses and displays them in the notebook. The spot.ltsmin 54 code that loads modules compiled with SpinS had to be rewritten to 55 capture and display the output of SpinS, so that our test-cases 56 can be reproduced regardless of the IPykernel version. This fix 57 was easier to do in Python 3.5. 58 59 - Fix sevaral minor documentation errors. 60 61New in spot 2.10 (2021-11-13) 62 63 Build: 64 65 - Spot is now built in C++17 mode, so you need at least GCC 7 or 66 clang 5 to compile it. The current versions of all major linux 67 distributions ship with at least GCC 7.4, so this should not be a 68 problem. There is also an --enable-c++20 option to configure in 69 case you want to force a build of Spot in C++20 mode. 70 71 Command-line tools: 72 73 - ltlsynt has been seriously overhauled, while trying to 74 preserve backward compatibility. Below is just a summary 75 of the main user-visible changes. Most of the new options 76 are discussed on https://spot-dev.lrde.epita.fr/ltlsynt.html 77 78 + ltlsynt now accepts only one of the --ins or --outs options to 79 be given and will deduce the value of the other one. 80 81 + ltlsynt learned --print-game-hoa to output its internal parity 82 game in the HOA format (with an extension described below). 83 84 + ltlsynt --aiger option now takes an optional argument indicating 85 how the bdd and states are to be encoded in the aiger output. 86 The option has to be given in the form 87 ite|isop|both[+ud][+dc][+sub0|sub1|sub2] where the first only 88 obligatory argument decides whether "if-then-else" ("ite") or 89 irreducible-sum-of-products ("isop") is to be used. "both" 90 executes both strategies and retains the smaller circuits. The 91 additional options are for fine-tuning. "ud" also encodes the 92 dual of the conditions and retains the smaller circuits. "dc" 93 computes if for some inputs we do not care whether the output is 94 high or low and try to use this information to compute a smaller 95 circuit. "subX" indicates different strategies to find common 96 subexpressions, with "sub0" indicating no extra computations. 97 98 + ltlsynt learned --verify to check the computed strategy or aiger 99 circuit against the specification. 100 101 + ltlsynt now has a --decompose=yes|no option to specify if 102 the specification should be decomposed into independent 103 sub-specifications, the controllers of which can then be glued 104 together to satisfy the input specification. 105 (cf. [finkbeiner.21.nfm] in doc/spot.bib) 106 107 + ltlsynt learned --simplify=no|bisim|bwoa|sat|bisim-sat|bwoa-sat 108 to specifies how to simplify the synthesized controler. 109 110 - ltl2tgba, autfilt, dstar2tgba, and randaut learned a --buchi 111 option, or -b for short. This outputs Büchi automata without 112 forcing state-based acceptance. 113 114 The following aliases have also been added for consistency: 115 --gba is an alias for --tgba, because the "t" of --tgba is 116 never forced. 117 --sba is an alias for -B/--ba, because -B really 118 implies -S and that is not clear from --ba. 119 As a consequence of the introduction of --sba, the option 120 --sbacc (an alias for --state-based-acceptance) cannot be 121 abbreviated as --sba anymore. 122 123 - autfilt learned a --kill-states=NUM[,NUM...] option. 124 125 - ltlcross, autcross, ltldo have learned shorthands for 126 the commands of Owl 21.0. For instance running 127 ltlcross 'owl-21 ltl2nba' ... 128 is equivalent to running 129 ltlcross '{owl-21 ltl2nba}owl-21 ltl2nba -f %f>%O' ... 130 131 Library: 132 133 - Spot now provides convenient functions to create and solve games. 134 (twaalgos/game.hh) and some additional functions for reactive 135 synthesis (twaalgos/synthesis.hh, twaalgos/mealy_machine.hh). 136 137 - A new class called aig represent an and-inverter-graphs, and is 138 currently used during synthesis. (twaalgos/aiger.hh) 139 140 - Some new *experimental* classes, called "twacube" and "kripkecube" 141 implement a way to store automata or Kripke structures without 142 using BDDs as labels. Instead they use a structure called cube, 143 that can only encode a conjunction of litterals. Avoiding BDDs 144 (or rather, avoiding the BuDDy library) in the API for automata 145 makes it possible to build multithreaded algorithms. 146 147 /!\ Currently these classes should be considered as experimental, 148 and their API is very likely to change in a future version. 149 150 Functions like twacube_to_twa(), twa_to_twacube(), can be used 151 to bridge between automata with BDD labels, and automata with 152 cube labels. 153 154 In addition to the previous conversion, we implemented various 155 state-of-the-art multi-threaded emptiness-check algorithms: 156 [bloemen.16.ppopp], [bloemen.16.hvc], [evangeslita.12.atva], 157 [renault.13.lpar], [holzmann.11.ieee] (see doc/spot.bib). 158 159 The mc_instanciator class provides an abstraction for launching, 160 pinning, and stopping threads inside of parallel model-checking 161 algorithms. 162 163 The class ltsmin_model class, providing support for loading 164 various models that follow ltsmin's PINS interinterface, has 165 been adjusted and can now produce either a kripke instance, or 166 a kripkecube instance. 167 168 - The postprocessor::set_type() method can now accept 169 options postprocessor::Buchi and postprocessor::GeneralizedBuchi. 170 171 These syntaxes is more homogeneous with the rest of the supported 172 types. Note that postprocessor::BA and postprocessor::TGBA, while 173 still supported and not yet marked as deprecated, are best avoided 174 in new code. 175 176 postprocessor::set_type(postprocessor::TGBA) 177 178 can be replaced by 179 180 postprocessor::set_type(postprocessor::GeneralizedBuchi) 181 182 and 183 184 postprocessor::set_type(postprocessor::BA) 185 186 by 187 188 postprocessor::set_type(postprocessor::Buchi) 189 postprocessor::set_pref(postprocessor::Small 190 | postprocessor::SBAcc) 191 192 Note that the old postprocessor::BA option implied state-based 193 acceptance (and was unique in that way), but the new 194 postprocessor::Buchi specifies Büchi acceptance without requiring 195 state-based acceptance (something that postprocessor did not 196 permit before). 197 198 - Translations for formulas such as FGp1 & FGp2 &...& FGp32 which 199 used to take ages are now instantaneous. (Issue #412.) 200 201 - remove_fin() learned to remove more unnecessary edges by using 202 propagate_marks_vector(), both in the general case and in the 203 Rabin-like case. 204 205 - simplify_acceptance() learned to simplify acceptence formulas of 206 the form Inf(x)&Inf(y) or Fin(x)|Fin(y) when the presence of x 207 always implies that of y. (Issue #406.) 208 209 - simplifiy_acceptance_here() and propagate_marks_here() learned to 210 use some patterns of the acceptance condition to remove or add 211 (depending on the function) colors on edges. As an example, with 212 a condition such as Inf(0) | Fin(1), an edge labeled by {0,1} can 213 be simplied to {0}, but the oppose rewriting can be useful as 214 well. (Issue #418.) 215 216 - The parity_game class has been removed, now any twa_graph_ptr that 217 has a "state-player" property is considered to be a game. 218 219 - the "state-player" property is output by the HOA printer, and read 220 back by the automaton parser, which means that games can be saved 221 and loaded. 222 223 - print_dot() will display states from player 1 using a diamond 224 shape. 225 226 - print_dot() learned to display automata that correspond to Mealy 227 machines specifically. 228 229 - print_dot() has a new option "i" to define id=... attributes for 230 states (S followed by the state number), edges (E followed by the 231 edge number), and SCCs (SCC followed by SCC number). The option 232 "i(graphid)" will also set the id of the graph. These id 233 attributes are useful if an automaton is converted into SVG and 234 one needs to refer to some particular state/edge/SCC with CSS or 235 javascript. See https://spot.lrde.epita.fr/oaut.html#SVG-and-CSS 236 237 - spot::postproc has new configuration variables that define 238 thresholds to disable some costly operation in order to speedup 239 the processing of large automata. (Those variables are typically 240 modified using the -x option of command-line tools, and are all 241 documented in the spot-x(7) man page.) 242 243 wdba-det-max Maximum number of additional states allowed in 244 intermediate steps of WDBA-minimization. If the 245 number of additional states reached in the 246 powerset construction or in the followup products 247 exceeds this value, WDBA-minimization is aborted. 248 Defaults to 4096. Set to 0 to disable. This limit 249 is ignored when -D used or when det-max-states is 250 set. 251 252 simul-max Number of states above which simulation-based 253 reductions are skipped. Defaults to 4096. Set 254 to 0 to disable. This also applies to the 255 simulation-based optimization of the 256 determinization algorithm. 257 258 simul-trans-pruning 259 For simulation-based reduction, this is the 260 number of equivalence classes above which 261 transition-pruning for non-deterministic automata 262 is disabled. Defaults to 512. Set to 0 to 263 disable. This applies to all simulation-based 264 reduction, as well as to the simulation-based 265 optimization of the determinization algorithm. 266 Simulation-based reduction perform a number of 267 BDD implication checks that is quadratic in the 268 number of classes to implement transition pruning. 269 270 dpa-simul Set to 0/1 to disable/enable simulation-based 271 reduction performed after running a Safra-like 272 determinization to optain a DPA. By default, it is 273 only disabled with --low or if simul=0. 274 275 dba-simul Set to 0/1 to disable/enable simulation-based 276 reduction performed after running the 277 powerset-like construction (enabled by option 278 tba-det) to obtain a DBA. By default, it is 279 only disabled with --low or if simul=0. 280 281 spot::translator additionally honor the following new variables: 282 283 tls-max-states Maximum number of states of automata involved in 284 automata-based implication checks for formula 285 simplifications. Defaults to 64. 286 287 exprop When set, this causes the core LTL translation to 288 explicitly iterate over all possible valuations of 289 atomic propositions when considering the successors 290 of a BDD-encoded state, instead of discovering 291 possible successors by rewriting the BDD as a sum of 292 product. This is enabled by default for --high, 293 and disabled by default otherwise. When unambiguous 294 automata are required, this option forced and 295 cannot be disabled. (This feature is not new, but 296 was not tunable before.) 297 298 - In addition the to above new variables, the default value for 299 ba-simul (controling how degeneralized automata are reduced) and 300 for det-simul (simulation-based optimization of the 301 determinization) is now equal to the default value of simul. This 302 changes allows "-x simul=0" to disable all of "ba-simul", 303 "dba-simul", "dpa-simul", and "det-simul" at once. 304 305 - tgba_powerset() now takes an extra optional argument to specify a 306 list of accepting sinks states if some are known. Doing so can 307 cut the size of the powerset automaton by 2^|sinks| in favorable 308 cases. 309 310 - twa_graph::merge_edges() had its two passes swapped. Doing so 311 improves the determinism of some automata. 312 313 - twa_graph::kill_state(num) is a new method that removes the 314 outgoing edge of some state. It can be used together with 315 purge_dead_states() to remove selected states. 316 317 - The new functions reduce_direct_sim(), reduce_direct_cosim() and 318 reduce_iterated() (and their state based acceptance version, 319 reduce_direct_sim_sba(), reduce_direct_cosim_sba() and 320 reduce_iterated_sba()), are matrix-based implementation of 321 simulation-based reductions. This new version is faster 322 than the signature-based BDD implementation in most cases, 323 however there are some cases it does not capture yet.. By 324 default, the old one is used. This behavior can be changed by 325 setting SPOT_SIMULATION_REDUCTION environment variable or using 326 the "-x simul-method=..." option (see spot-x(7)). 327 328 - The automaton parser will now recognize lines of the form 329 #line 10 "filename" 330 that may occur *between* the automata of an input stream to specify 331 that error messages should be emitted as if the next automaton 332 was read from "filename" starting on line 10. (Issue #232) 333 334 - The automaton parser for HOA is now faster at parsing files where 335 a label is used multiple times (i.e., most automata): it uses a 336 hash table to avoid reconstructing BDDs corresponding to label 337 that have already been parsed. This trick was already used in the 338 never claim parser. 339 340 - spot::twa_graph::merge_states() will now sort the vector of edges 341 before attempting to detect mergeable states. When merging states 342 with identical outgoing transitions, it will now also consider 343 self-looping transitions has having identical destinations. 344 Additionally, this function now returns the number of states that 345 have been merged (and therefore removed from the automaton). 346 347 - spot::zielonka_tree and spot::acd are new classes that implement the 348 Zielonka Tree and Alternatic Cycle Decomposition, based on a paper 349 by Casares et al. (ICALP'21). Those structures can be used to 350 paritize any automaton, and more. The graphical rendering of ACD 351 in Jupyter notebooks is Spot's first interactive output. See 352 https://spot.lrde.epita.fr/ipynb/zlktree.html for more. 353 354 Python: 355 356 - Bindings for functions related to games. 357 See https://spot.lrde.epita.fr/ipynb/games.html and 358 https://spot.lrde.epita.fr/tut40.html for examples. 359 360 - Bindings for functions related to synthesis and aig-circuits. 361 See https://spot.lrde.epita.fr/ipynb/synthesis.html 362 363 - spot::twa::prop_set was previously absent from the Python 364 bindings, making it impossible to call make_twa_graph() for copying 365 a twa. It is now available as spot.twa_prop_set (issue #453). 366 Also for convenience, the twa_graph.__copy__() method, called by 367 copy.copy(), will duplicate a twa_graph (issue #470). 368 369 Bugs fixed: 370 371 - tgba_determinize() could create parity automata using more colors 372 than necessary. (Related to issue #298) 373 374 - There were two corners cases under which sat_minimize() would 375 return the original transition-based automaton when asked to 376 produce state-based output without changing the acceptance 377 condition. 378 379 Deprecation notices: 380 381 - twa_graph::defrag_states() and digraph::defrag_states() now take 382 the renaming vector by reference instead of rvalue reference. The 383 old prototype is still supported but will emit a deprecation 384 warning. 385 386New in spot 2.9.8 (2021-08-10) 387 388 Documentation: 389 390 - Mention the conda-forge package. 391 392 Bugs fixed: 393 394 - left->intersacting_run(right) could return a run with incorrect 395 colors (likely not corresponding to any existing transition of 396 left) if left was a weak automaton. (Issue #471) 397 398 - Fix bitset::operator-() causing issues when Spot was configured 399 with more than 32 colors for instance with --enable-max-sets=64. 400 (Issue #469) 401 402 - Work around some warnings from newer compilers. 403 404 405New in spot 2.9.7 (2021-05-12) 406 407 Bugs fixed: 408 409 - Some formulas using ->, <->, or xor were not properly detected as 410 purely universal or pure eventualities. 411 412 - autfilt --keep-states=... could incorrectly mention --mask-acc 413 when diagnosing errors. 414 415 - Work around GraphViz issue 1931, causing spurious failures in the 416 test suite. 417 418 - Miscelaneous documentation fixes. 419 420New in spot 2.9.6 (2021-01-18) 421 422 Build: 423 424 - Build scripts are now compatible with Autoconf 2.70 (Issue #447) 425 and require at least Autoconf 2.69 (released in 2012). 426 427 - Debian builds use updated standards. 428 429 Bugs fixed: 430 431 - twa_graph::merge_edges() could fail to merge two transitions if the 432 destination transition was the first of the automaton. (Issue #441) 433 434 - On non-deterministic automata, iterated_simulations() was 435 performing an (unnecessary) second iteration even when the first 436 one failed to reduce the automaton. (Issue #442) 437 438 - When passed an incomplete automaton as input, tgba_determinize() 439 would sometimes produce a complete automaton but incorrectly mark 440 it as incomplete. (Related to issue #298) 441 442 - gf_guarantee_to_ba(), used to translate some specific classes of 443 subformulas, could segfault in some condition (Issue #449). 444 445 - Work around some spurious test suite failures. 446 447New in spot 2.9.5 (2020-11-19) 448 449 Bugs fixed: 450 451 - Fix multiple spurious test suite failures on Darwin 452 (Issues #426, #427, #428, #429) or when the 453 Pandas package was not installed. 454 455 - The filename python/spot/aux.py caused a problem on Windows and 456 has been renamed. Existing "import spot.aux" statements should 457 *not* be updated. (Issue #437) 458 459 - Fix memory leak in minimize_wdba() when determinization is aborted 460 because an output_aborter is passed. 461 462 - Distribution used to contain unnecessary large SVG files (Issue #422) 463 464New in spot 2.9.4 (2020-09-07) 465 466 Bugs fixed: 467 468 - Handle xor and <-> in a more natural way when translating 469 LTL formulas to generic acceptance conditions. 470 471 - Multiple typos in documentation, --help texts, or error messages. 472 473New in spot 2.9.3 (2020-07-22) 474 475 Bug fixed: 476 477 - Completely fix the ltlcross issue mentioned in previous release. 478 479New in spot 2.9.2 (2020-07-21) 480 481 Bugs fixed: 482 483 - ltlcross --csv=... --product=N with N>0 could output spurious 484 diagnostics claiming that words were rejected when evaluating 485 the automaton on state-space. 486 487 - spot::scc_info::determine_unknown_acceptance() now also update the 488 result of spot::scc_info::one_accepting_scc(). 489 490New in spot 2.9.1 (2020-07-15) 491 492 Command-line tools: 493 494 - 'ltl2tgba -G -D' is now better at handling formulas that use 495 '<->' and 'xor' operators at the top level. For instance 496 ltl2tgba -D -G '(Fa & Fb & Fc & Fd) <-> GFe' 497 now produces a 16-state automaton (instead of 31 in Spot 2.9). 498 499 - Option '-x wdba-minimize=N' used to accept N=0 (off), or N=1 (on). 500 It can now take three values: 501 0: never attempt this optimization, 502 1: always try to determinize and minimize automata as WDBA, 503 and check (if needed) that the result is correct, 504 2: determinize and minimize automata as WDBA only if it is known 505 beforehand (by cheap syntactic means) that the result will be 506 correct (e.g., the input formula is a syntactic obligation). 507 The default is 1 in "--high" mode, 2 in "--medium" mode or in 508 "--deterministic --low" mode, and 0 in other "--low" modes. 509 510 - ltlsynt learned --algo=ps to use the default conversion to 511 deterministic parity automata (the same as ltl2tgba -DP'max odd'). 512 513 - ltlsynt now has a -x option to fine-tune the translation. See the 514 spot-x(7) man page for detail. Unlike ltl2tgba, ltlsynt defaults 515 to simul=0,ba-simul=0,det-simul=0,tls-impl=1,wdba-minimize=2. 516 517 Library: 518 519 - product_xor() and product_xnor() are two new versions of the 520 synchronized product. They only work with operands that are 521 deterministic automata, and build automata whose language are 522 respectively the symmetric difference of the operands, and the 523 complement of that. 524 525 - tl_simplifier_options::keep_top_xor is a new option to keep Xor 526 and Equiv operator that appear at the top of LTL formulas (maybe 527 below other Boolean or X operators). This is used by the 528 spot::translator class when creating deterministic automata with 529 generic acceptance. 530 531 - remove_fin() learned a trick to remove some superfluous 532 transitions. 533 534 Bugs fixed: 535 536 - Work around undefined behavior reported by clang 10.0.0's UBsan. 537 538 - spot::twa_sub_statistics was very slow at computing the number of 539 transitons, and could overflow. It is now avoiding some costly 540 loop of BDD operations, and storing the result using at least 64 541 bits. This affects the output of "ltlcross --csv" and 542 "--stats=%t" for many tools. 543 544 - simplify_acceptance() missed some patterns it should have been 545 able to simplify. For instance Fin(0)&(Fin(1)|Fin(2)|Fin(4)) 546 should simplify to Fin(1)|Fin(2)|Fin(4) after adding {1,2,4} to 547 every place where 0 occur, and then the acceptance would be 548 renumbered to Fin(0)|Fin(1)|Fin(2). This is now fixed. 549 550 - Improve ltldo diagnostics to fix spurious test-suite failure on 551 systems with antique GNU libc. 552 553 - twa_run::reduce() could reduce accepting runs incorrectly on 554 automata using Fin in their acceptance condition. This caused 555 issues in intersecting_run(), exclusive_run(), 556 intersecting_word(), exclusive_word(), which all call reduce(). 557 558 - ltlcross used to crash with "Too many acceptance sets used. The 559 limit is 32." when complementing an automaton would require more 560 acceptance sets than supported by Spot. This is now diagnosed 561 with --verbose, but does not prevent ltlcross from continuing. 562 563 - scc_info::edges_of() and scc_info::inner_edges_of() now correctly 564 honor any filter passed to scc_info. 565 566New in spot 2.9 (2020-04-30) 567 568 Command-line tools: 569 570 - When the --check=stutter-sensitive-example option is passed to 571 tools like ltl2tgba, autfilt, genaut, or ltldo, the produced 572 automata are checked for stutter-invariance (as in the 573 --check=stutter-invariant case), additionally a proof of 574 stutter-sensitiveness is provided as two stutter-equivalent words: 575 one accepted, and one rejected. These sample words are printed in 576 the HOA output. 577 578 % ltl2tgba --check=stutter-sensitive-example Xa | grep word: 579 spot-accepted-word: "!a; cycle{a}" 580 spot-rejected-word: "!a; !a; cycle{a}" 581 582 - autfilt learned the --partial-degeneralize option, to remove 583 conjunctions of Inf, or disjunctions of Fin that appears in 584 arbitrary conditions. 585 586 - ltlfilt and autfilt learned a --nth=RANGE (a.k.a. -N) option to 587 select a range of their input formulas or automata (assuming a 588 1-based numbering). 589 590 - When running translators, ltlcross will now display {names} when 591 supplied. 592 593 - ltlcross is now using the generic emptiness check procedure 594 introduced in Spot 2.7, as opposed to removing Fin acceptance 595 before using a classical emptiness check. 596 597 - ltlcross learned a --save-inclusion-products=FILENAME option. Its 598 use cases are probably quite limited. We use that to generate 599 benchmarks for our generic emptiness check procedure. 600 601 - ltlsynt --algo=lar uses the new version of to_parity() mentionned 602 below. The old version is available via --algo=lar.old 603 604 - ltlsynt learned --csv=FILENAME, to record some statistics about 605 the duration of its different phases. 606 607 - The dot printer is now automatically using rectangles with rounded 608 corners for automata states if one state label have five or more 609 characters. This saves space with very long labels. Use --dot=c, 610 --dot=e, or --dot=E to force the use of Circles, Ellipses, or 611 rEctangles. 612 613 Library: 614 615 - Historically, Spot only supports LTL with infinite semantics 616 so it had automatic simplifications reducing X(1) and X(0) to 617 1 and 0 whenever such formulas are constructed. This 618 caused issues for users of LTLf formulas, where it is important 619 to distinguish a "weak next" (for which X(1)=1 but X(0)!=0) from 620 a "strong next" (for which X(0)=0 but X(1)!=1). 621 622 To accommodate this, this version introduces a new operator 623 op::strong_X in addition to the existing op::X (whose 624 interpretation is now weak in LTLf). The syntax for the strong 625 next is X[!] as a reference to the PSL syntax (where the strong 626 next is written X!). 627 628 Trivial simplification rules for X are changed to just 629 X(1) = 1 (and not X(0)=0 anymore) 630 while we have 631 X[!]0 = 0 632 633 The X(0)=0 and X[!]1=1 reductions are now preformed during LTL 634 simplification, not automatically. Aside from the from_ltlf() 635 function, the other functions of the library handle X and X[!] in 636 the same way, since there is no difference between X and X[!] over 637 infinite words. 638 639 Operators F[n:m!] and G[n:m!] are also supported as strong 640 variants of F[n:m] and G[n:m], but those four are only implemented 641 as syntactic sugar. 642 643 - acc_cond::acc_code::parity(bool, bool, int) was not very readable, 644 as it was unclear to the reader what the boolean argument meant. 645 The following sister functions can now improve readability: 646 parity_max(is_odd, n) = parity(true, is_odd, n) 647 parity_max_odd(n) = parity_max(true, n) 648 parity_max_even(n) = parity_max(false, n) 649 parity_min(is_odd, n) = parity(false, is_odd, n) 650 parity_min_odd(n) = parity_min(true, n) 651 parity_min_even(n) = parity_min(false, n) 652 653 - partial_degeneralize() is a new function performing partial 654 degeneralization to get rid of conjunctions of Inf terms, or 655 disjunctions of Fin terms in acceptance conditions. 656 657 - simplify_acceptance_here() and simplify_acceptance() learned to 658 simplify subformulas like Fin(i)&Fin(j) or Inf(i)|Inf(j), or some 659 more complex variants of those. If i is uniquely used in the 660 acceptance condition, these become respectively Fin(i) or Inf(i), 661 and the automaton is adjusted so that i also appears where j 662 appeared. 663 664 - acc_code::unit_propagation() is a new method for performing unit 665 propagation in acceptance condition. E.g. Fin(0) | (Inf(0) & 666 Inf(1)) becomes Fin(0) | Inf(1). This is now called by 667 simplify_acceptance_here(). 668 669 - propagate_marks_vector() and propagate_marks_here() are helper 670 functions for propagating marks on the automaton: ignoring 671 self-loops and out-of-SCC transitions, marks common to all the 672 input transitions of a state can be pushed to all its outgoing 673 transitions, and vice-versa. This is repeated until a fix point 674 is reached. propagate_marks_vector() does not modify the 675 automaton and returns a vector of the acc_cond::mark_t that should 676 be on each transition; propagate_marks_here() actually modifies 677 the automaton. 678 679 - rabin_to_buchi_if_realizable() is a new variant of 680 rabin_to_buchi_maybe() that converts a Rabin-like automaton into a 681 Büchi automaton only if the resulting Büchi automaton can keep the 682 same transition structure (where the ..._maybe() variant would 683 modify the Rabin automaton if needed). 684 685 - to_parity() has been rewritten. It now combines several strategies 686 for paritizing automata with any acceptance condition. 687 688 - relabel_bse(), used by ltlfilt --relabel-bool, is now better at 689 dealing with n-ary operators and isolating subsets of operands 690 that can be relabeled as a single term. 691 692 - print_dot()'s default was changed to use circles for automata with 693 fewer than 10 unamed states, ellipses for automata with up to 1000 694 unamed states (or named states with up to 4 characters), and 695 rounded rectangles otherwise. Rectangles are also used for 696 automata with acceptance bullets on states. The new "E" option 697 can be used to force rectangles in all situations. 698 699 - The generic emptiness check has been slightly improved (doing 700 fewer recursive calls in the worst case). 701 702 Backward-incompatible changes: 703 704 - iar() and iar_maybe() have been moved from 705 spot/twaalgos/rabin2parity.hh spot/twaalgos/toparity.hh and marked 706 as deprecated, they should be replaced by to_parity(). In case 707 the input is Rabin-like or Streett-like, to_parity() should be at 708 least as good as iar(). 709 710 - The twa_graph::is_alternating() and digraph::is_alternating() methods, 711 deprecated in Spot 2.3.1 (2017-02-20), have been removed. 712 713 Bugs fixed: 714 715 - Relabeling automata could introduce false edges. Those are now 716 removed. 717 718 - Emptiness checks, and scc_info should now ignore edges labeled 719 with false. 720 721 - relabel_bse() could incorrectly relabel Boolean subformulas that 722 had some atomic propositions in common. 723 724New in spot 2.8.7 (2020-03-13) 725 726 Bugs fixed: 727 728 - Building a product between two complete automata where one operand 729 had false acceptance could create an incomplete automaton 730 incorrectly tagged as complete, causing the print_hoa() function 731 to raise an exception. 732 733 - autfilt --uniq was not considering differences in acceptance 734 conditions or number of states when discarding automata. 735 736 - In an automaton with acceptance condition containing some Fin, and 737 whose accepting cycle could be reduced to a self-loop in an 738 otherwise larger SCC, the generation of an accepting run could be 739 wrong. This could in turn cause segfaults or infinite loops while 740 running autcross or autfilt --stats=%w. 741 742 - The generic emptiness check used a suboptimal selection of "Fin" 743 to remove, not matching the correct line in our ATVA'19 paper. 744 This could cause superfluous recursive calls, however benchmarks 745 have shown the difference to be insignificant in practice. 746 747 - The sl(), and sl2() functions for computing the "self-loopization" 748 of an automaton, and used for instance in algorithms for computing 749 proof of stutter-sensitiveness (e.g., in our web application), 750 were incorrect when applied on automata with "t" acceptance (or 751 more generaly, any automaton where a cycle without mark is 752 accepting). 753 754 - ltlcross was not diagnosing write errors associated to 755 options --grind=FILENAME and --save-bogus=FILENAME. 756 757New in spot 2.8.6 (2020-02-19) 758 759 Bugs fixed: 760 761 - calling spot.translate() with two conflicting preferences like 762 spot.translate(..., 'det', 'any') triggered a syntax error in the 763 Python code to handle this error. 764 765 - degeneralize_tba() was incorrectly not honnoring the "skip_level" 766 optimization after creating an accepting transition; as a 767 consequence, some correct output could be larger than necessary 768 (but still correct). 769 770 - Some formulas with Boolean sub-formulas equivalent to true or 771 false could be translated into automata with false labels. 772 773 - The HOA printer would incorrectly output the condition such 774 'Fin(1) & Inf(2) & Fin(0)' as 'Fin(0) | Fin(1) & Inf(2)' 775 due to a bug in the is_generalized_rabin() matching function. 776 777New in spot 2.8.5 (2020-01-04) 778 779 Bugs fixed: 780 781 - ltl2tgba -B could return automata with "t" acceptance, instead 782 of the expected Inf(0). 783 784 - twa_graph::merge_edges() (a.k.a. autfilt --merge-transitions) was 785 unaware that merging edges can sometimes transform a 786 non-deterministic automaton into a deterministic one, causing the 787 following unexpected diagnostic: 788 "print_hoa(): automaton is universal despite prop_universal()==false" 789 The kind of non-deterministic automata where this occurs is not 790 naturally produced by any Spot algorithm, but can be found for 791 instance in automata produced by Goal 2015-10-18. 792 793New in spot 2.8.4 (2019-12-08) 794 795 Bugs fixed: 796 797 - The Rabin-to-Büchi conversion could misbehave when applied to 798 Rabin-like acceptance with where some pairs have missing Inf(.) 799 (e.g. Fin(0)|(Inf(1)&Fin(2))) and when some of the SCCs do not 800 visit the remaining Inf(.). This indirectly caused the 801 complementation algorithm to produce incorrect results on such 802 inputs, causing false positives in ltlcross and autcross. 803 804 - Work around a small difference between Python 3.7 and 3.8, causing 805 spurious failures of the test suite. 806 807New in spot 2.8.3 (2019-11-06) 808 809 Build: 810 811 - Minor portabilities improvements with C++17 deprecations. 812 813 Python: 814 815 - Doing "import spot.foo" will now load any spot-extra/foo.py on 816 Python's search path. This can be used to install third-party 817 packages that want to behave as plugins for Spot. 818 819 - Work around GraphViz bug #1605 in Jupyter notebooks. 820 https://gitlab.com/graphviz/graphviz/issues/1605 821 822New in spot 2.8.2 (2019-09-27) 823 824 Command-line tools: 825 826 - ltl2tgba and ltldo learned a --negate option. 827 828 Bugs fixed: 829 830 - Calling "autfilt --dualize" on an alternating automaton with 831 transition-based acceptance and universal initial states would 832 fail with "set_init_state() called with nonexisting state". 833 834 - The numbering of nodes in the AIGER output of ltlsynt was 835 architecture dependent. 836 837 - Various compilation issues. In particular, this release is the 838 first one that can be compiled (and pass tests) on a Raspberry PI. 839 840New in spot 2.8.1 (2019-07-18) 841 842 Command-line tools: 843 844 - genltl learned --pps-arbiter-standard and --pps-arbiter-strict. 845 846 - ltlcross and autcross have learned a new option -q (--quiet) to 847 remain quiet until an error is found. This helps for instance in 848 scenarios where multiple instances of ltlcross/autcross are run in 849 parallel (using "xargs -P" or "GNU Parallel", for instance). See 850 https://spot.lrde.epita.fr/ltlcross.html#parallel for examples. 851 852 Bugs fixed: 853 854 - When complement() was called with an output_aborter, it could 855 return an alternating automaton on large automata. This in turn 856 caused ltlcross to emit errors like "remove_alternation() only 857 works with weak alternating automata" or "product() does not 858 support alternating automata". 859 860 - Work around Emacs bug #34341 when rebuilding documentation on a 861 system with Emacs <26.3, GNU TLS >= 3.6, and without ESS or with 862 an obsolete org-mode installed. 863 864New in spot 2.8 (2019-07-10) 865 866 Command-line tools: 867 868 - autfilt learned --highlight-accepting-run=NUM to highlight some 869 accepting run with color NUM. 870 871 - ltldo, ltlcross, and autcross are now preferring posix_spawn() 872 over fork()+exec() when available. 873 874 - ltlcross has new options --determinize-max-states=N and 875 --determinize-max-edges=M to restrict the use of 876 determinization-based complementation to cases where it produces 877 automata with at most N states and M edges. By default 878 determinization is now attempted up to 500 states and 5000 879 edges. This is an improvement over the previous default where 880 determinization-based complementation was not performed at all, 881 unless -D was specified. 882 883 - ltlcross will now skip unnecessary cross-checks and 884 consistency-checks (they are unnecessary when all automata 885 could be complemented and statistics were not required). 886 887 - genaut learned --m-nba=N to generate Max Michel's NBA family. 888 (NBAs with N+1 states whose determinized have at least N! states.) 889 890 - Due to some new simplification of parity acceptance, the output of 891 "ltl2tgba -P -D" is now using a minimal number of colors. This 892 means that recurrence properties have an acceptance condition 893 among "Inf(0)", "t", or "f", and persistence properties have an 894 acceptance condition among "Fin(0)", "t", or "f". 895 896 - ltldo and ltlcross learned shorthands to call the tools ltl2na, 897 ltl2nba, and ltl2ngba from Owl 19.06. Similarly, autcross learned 898 a shorthand for Owl's dra2dpa. 899 900 Documentation: 901 902 - https://spot.lrde.epita.fr/tut90.html is a new file that explains 903 the purpose of the spot::bdd_dict object. 904 905 Library: 906 907 - Add generic_accepting_run() as a variant of generic_emptiness_check() that 908 returns an accepting run in an automaton with any acceptance condition. 909 910 - twa::accepting_run() and twa::intersecting_run() now work on 911 automata using Fin in their acceptance condition. 912 913 - simulation-based reductions have learned a trick that sometimes 914 improve transition-based output when the input is state-based. 915 (The automaton output by 'ltl2tgba -B GFa | autfilt --small' now 916 has 1 state instead of 2 in previous versions. Similarly, 917 'ltldo ltl2dstar -f 'GFa -> GFb' | autfilt --small' produces 1 918 state instead of 4.) 919 920 - simulation-based reductions has learned another trick to better 921 merge states from transient SCCs. 922 923 - acc_cond::top_disjuncts() and acc_cond::top_conjuncts() can be 924 used to split an acceptance condition on the top-level & or |. 925 These methods also exist in acc_cond::acc_code. 926 927 - minimize_obligation() learned to work on very weak automata even 928 if the formula or negated automaton are not supplied. (This 929 allows "autfilt [-D] --small" to minimize very-weak automata 930 whenever they are found to represent obligation properties.) 931 932 - There is a new spot::scc_and_mark_filter object that simplifies the 933 creation of filters to restrict spot::scc_info to some particular 934 SCC while cutting new SCCs on given acceptance sets. This is used 935 by spot::generic_emptiness_check() when processing SCCs 936 recursively, and makes it easier to write similar code in Python. 937 938 - print_dot has a new option 'g', to hide edge labels. This is 939 helpful to display automata as "graphs", e.g., when illustrating 940 algorithms that do not care about labels. 941 942 - A new complement() function returns complemented automata with 943 unspecified acceptance condition, allowing different algorithms to 944 be used. The output can be alternating only if the input was 945 alternating. 946 947 - There is a new class output_aborter that is used to specify 948 upper bounds on the size of automata produced by some algorithms. 949 Several functions have been changed to accept an output_aborter. 950 This includes: 951 * tgba_determinize() 952 * tgba_powerset() 953 * minimize_obligation() 954 * minimize_wdba() 955 * remove_alternation() 956 * product() 957 * the new complement() 958 * the postprocessor class, via the "det-max-state" and 959 "det-max-edges" options. 960 961 - SVA's first_match operator can now be used in SERE formulas and 962 that is supported by the ltl_to_tgba_fm() translation. See 963 doc/tl/tl.pdf for the semantics. *WARNING* Because this adds a 964 new operator, any code that switches over the spot::op type may 965 need a new case for op::first_match. Furthermore, the output of 966 "randltl --psl" will be different from previous releases. 967 968 - The parser for SERE learned to recognize the ##n and ##[i:j] 969 operators from SVA. So {##2 a ##0 b[+] ##1 c ##2 e} is another 970 way to write {[*2];a:b[+];c;1;e}. The syntax {a ##[i:j] b} is 971 replaced in different ways depending on the values of i, a, and b. 972 The formula::sugar_delay() function implements this SVA operator in 973 terms of the existing PSL operators. ##[+] and ##[*] are sugar 974 for ##[1:$] and ##[0:$]. 975 976 - The F[n:m] and G[n:m] operators introduced in Spot 2.7 now 977 support the case where m=$. 978 979 - spot::relabel_apply() makes it easier to reverse the effect 980 of spot::relabel() or spot::relabel_bse() on formula. 981 982 - The LTL simplifier learned the following rules: 983 F(G(a | Fb)) = FGa | GFb (if option "favor_event_univ") 984 G(F(a | Gb)) = GFa | FGb (if option "favor_event_univ") 985 F(G(a & Fb) = FGa & GFb (unless option "reduce_size_strictly") 986 G(F(a & Gb)) = GFa & FGb (unless option "reduce_size_strictly") 987 GF(f) = GF(dnf(f)) (unless option "reduce_size_strictly") 988 FG(f) = FG(cnf(f)) (unless option "reduce_size_strictly") 989 (f & g) R h = f R h if h implies g 990 (f & g) M h = f M h if h implies g 991 (f | g) W h = f W h if g implies h 992 (f | g) U h = f U h if g implies h 993 Gf | F(g & eventual) = f W (g & eventual) if !f implies g 994 Ff & G(g | universal) = f M (g | universal) if f implies !g 995 f U (g & eventual) = F(g & eventual) if !f implies g 996 f R (g | universal) = G(g | universal) if f implies !g 997 998 - cleanup_parity() and colorize_parity() were cleaned up a bit, 999 resulting in fewer colors used in some cases. In particular, 1000 colorize_parity() learned that coloring transient edges does not 1001 require the introduction of a new color. 1002 1003 - A new reduce_parity() function implements and generalizes the 1004 algorithm for minimizing parity acceptance by Carton and Maceiras 1005 (Computing the Rabin index of a parity automaton, 1999). This is 1006 a better replacement for cleanup_parity() and colorize_parity(). 1007 See https://spot.lrde.epita.fr/ipynb/parity.html for examples. 1008 1009 - The postprocessor and translator classes are now using 1010 reduce_parity() for further simplifications. 1011 1012 - The code for checking recurrence/persistence properties can also 1013 use the fact the reduce_parity() with return "Inf(0)" (or "t" or 1014 "f") for deterministic automata corresponding to recurrence 1015 properties, and "Fin(0)" (or "t" or "f") for persistence 1016 properties. This can be altered with the SPOT_PR_CHECK 1017 environment variable. 1018 1019 Deprecation notices: 1020 1021 - The virtual function twa::intersecting_run() no longer takes a 1022 second "from_other" Boolean argument. This is a backward 1023 incompatibility only for code that overrides this function in a 1024 subclass. For backward compatibility with programs that simply 1025 call this function with two argument, a non-virtual version of the 1026 function has been introduced and marked as deprecated. 1027 1028 - The spot::acc_cond::format() methods have been deprecated. These 1029 were used to display acceptance marks, but acceptance marks are 1030 unrelated to acceptance conditions, so it's better to simply print 1031 marks with operator<< without this extra step. 1032 1033 Bugs fixed: 1034 1035 - The gf_guarantee_to_ba() is relying on an in-place algorithm that 1036 could produce a different number of edges for the same input in 1037 two different transition order. 1038 1039 - A symmetry-based optimization of the LAR algorithm performed in 1040 spot::to_parity() turned out to be incorrect. The optimization 1041 has been removed. "ltlsynt --algo=lar" is the only code using 1042 this function currently. 1043 1044New in spot 2.7.5 (2019-06-05) 1045 1046 Build: 1047 1048 - Although the Python bindings in this release are still done with 1049 Swig3.0, the code has been updated to be compatible with Swig4.0. 1050 1051 Library: 1052 1053 - print_dot will replace labels that have more 2048 characters by a 1054 "(label too long)" string. This works around a limitation of 1055 GraphViz that aborts when some label exceeds 16k characters, and 1056 also helps making large automata more readable. 1057 1058 Bugs fixed: 1059 1060 - spot::translator was not applying Boolean sub-formula rewriting 1061 by default unless a spot::option_map was passed. This caused some 1062 C++ code for translating certain formulas to be noticeably slower 1063 than the equivalent call to the ltl2tgba binary. 1064 1065 - The remove_ap algorithm was preserving the "terminal property" of 1066 automata, but it is possible that a non-terminal input produces a 1067 terminal output after some propositions are removed. 1068 1069New in spot 2.7.4 (2019-04-27) 1070 1071 Bugs fixed: 1072 1073 - separate_sets_here() (and therefore autfilt --separate-sets) could 1074 loop infinitely on some inputs. 1075 1076 - In some situation, ltl2tgba -G could abort with 1077 "direct_simulation() requires separate Inf and Fin sets". This 1078 was fixed by teaching simulation-based reductions how to deal 1079 with such cases. 1080 1081 - The code for detecting syntactically stutter-invariant PSL 1082 formulas was incorrectly handling the ";" operator, causing some 1083 stutter-sensitive formulas to be flagged a stutter-invariant. 1084 1085New in spot 2.7.3 (2019-04-19) 1086 1087 Bugs fixed: 1088 1089 - When processing CSV files with MSDOS-style \r\n line endings, 1090 --stats would output the \r as part of the %> sequence instead 1091 of ignoring it. 1092 1093 - Fix serious typo in remove_alternation() causing incorrect 1094 output for some VWAA. Bug introduced in Spot 2.6. 1095 1096 Documentation: 1097 1098 - Multiple typos and minor updates. 1099 1100New in spot 2.7.2 (2019-03-17) 1101 1102 Python: 1103 1104 - Improved support for explicit Kripke structures. It is now 1105 possible to iterate over a kripke_graph object in a way similar to 1106 twa_graph. 1107 1108 Documentation: 1109 1110 - A new page shows how to create explicit Kripke structures in C++ 1111 and Python. See https://spot.lrde.epita.fr/tut52.html 1112 - Another new page shows how to deal with LTLf formulas (i.e., LTL 1113 with finite semantics) and how to translate those. 1114 See https://spot.lrde.epita.fr/tut12.html 1115 1116 Build: 1117 1118 - Work around a spurious null dereference warning when compiling 1119 with --coverage and g++ 8.3.0-3 from Debian unstable. 1120 1121New in spot 2.7.1 (2019-02-14) 1122 1123 Build: 1124 1125 - Work around GCC bug #89303 that causes memory leaks and std::weak_bad_ptr 1126 exceptions when Spot is compiled with the version of g++ 8.2 currently 1127 distributed by Debian unstable (starting with g++ 8.2.0-15). 1128 1129 Python: 1130 1131 - The following methods of spot::bdd_dict are now usable in Python when 1132 fine control over the lifetime of associations between BDD variables 1133 and atomic propositions is needed. 1134 - register_proposition(formula, for_me) 1135 - register_anonymous_variables(count, for_me) 1136 - register_all_propositions_of(other, for_me) 1137 - unregister_all_my_variables(for_me) 1138 - unregister_variable(var, for_me) 1139 1140 - Better support for explicit Kripke structures: 1141 - the kripke_graph type now has Python bindings 1142 - spot.automaton() and spot.automata() now support a want_kripke=True 1143 to return a kripke_graph 1144 See the bottom of https://spot.lrde.epita.fr/ipynb/ltsmin-dve.html 1145 for some examples. 1146 1147 Library: 1148 1149 - Printing Kripke structures via print_hoa() will save state names. 1150 1151 - kripke_graph_ptr objects now honor any "state-names" property 1152 when formatting states. 1153 1154 Bugs fixed: 1155 1156 - The print_dot_psl() function would incorrectly number all but the 1157 first children of commutative n-ary operators: in this case no 1158 numbering was expected. 1159 1160 - std::out_of_range C++ exceptions raised from Python code are now 1161 converted into IndexError Python exceptions (instead of aborting 1162 the program). 1163 1164 - The LTL parser would choke on carriage returns when command-line 1165 tools such as ltlfilt, ltlcross, or ltl2tgba were run on files of 1166 formulas with MS-DOS line endings. 1167 1168 - The core translation for unambiguous automata was incorrectly 1169 tagging some non-weak automata as weak. 1170 1171 - The product_susp() function used to multiply an automaton with a 1172 suspendable automaton could incorrectly build transition-based 1173 automata when multiplying two state-based automata. This caused 1174 ltl2tgba to emit error messages such as: "automaton has 1175 transition-based acceptance despite prop_state_acc()==true". 1176 1177New in spot 2.7 (2018-12-11) 1178 1179 Command-line tools: 1180 1181 - ltlsynt now has three algorithms for synthesis: 1182 --algo=sd is the historical one. The automaton of the formula 1183 is split to separate inputs and outputs, then 1184 determinized (with Safra construction). 1185 --algo=ds the automaton of the formula is determinized (Safra), 1186 then split to separate inputs and outputs. 1187 --algo=lar translate the formula to a deterministic automaton 1188 with an arbitrary acceptance condition, then turn it 1189 into a parity automaton using LAR, and split it. 1190 In all three cases, the obtained parity game is solved using 1191 Zielonka algorithm. Calude's quasi-polynomial time algorithm has 1192 been dropped as it was not used. 1193 1194 - ltlfilt learned --liveness to match formulas representing liveness 1195 properties. 1196 1197 - the --stats= option of tools producing automata learned how to 1198 tell if an automaton uses universal branching (%u), or more 1199 precisely how many states (%[s]u) or edges (%[e]u) use universal 1200 branching. 1201 1202 Python: 1203 1204 - spot.translate() and spot.postprocess() now take an xargs= 1205 argument similar to the -x option of ltl2tgba and autfilt, making 1206 it easier to fine tune these operations. For instance 1207 ltl2tgba 'GF(a <-> XXa)' --det -x gf-guarantee=0 1208 would be written in Python as 1209 spot.translate('GF(a <-> XXa)', 'det', xargs='gf-guarantee=0') 1210 (Note: those extra options are documented in the spot-x(7) man page.) 1211 1212 - spot.is_generalized_rabin() and spot.is_generalized_streett() now return 1213 a tuple (b, v) where b is a Boolean, and v is the vector of the sizes 1214 of each generalized pair. This is a backward incompatible change. 1215 1216 Library: 1217 1218 - The LTL parser learned syntactic sugar for nested ranges of X 1219 using the X[n], F[n:m], and G[n:m] syntax of TSLF. (These 1220 correspond to the next!, next_e!, and next_a! operators of PSL, 1221 but we do not support those under these names currently.) 1222 1223 X[6]a = XXXXXXa 1224 F[2:4]a = XX(a | X(a | Xa)) 1225 G[2:4]a = XX(a & X(a & Xa)) 1226 1227 The corresponding constructors (for C++ and Python) are 1228 formula::X(unsigned, formula) 1229 formula::F(unsigned, unsigned, formula) 1230 formula::G(unsigned, unsigned, formula) 1231 1232 - spot::unabbreviate(), used to rewrite away operators such as M or 1233 W, learned to use some shorter rewritings when an argument (e) is 1234 a pure eventuality or (u) is purely universal: 1235 1236 Fe = e 1237 Gu = u 1238 f R u = u 1239 f M e = F(f & e) 1240 f W u = G(f | u) 1241 1242 - The twa_graph class has a new dump_storage_as_dot() method 1243 to show its data structure. This is more conveniently used 1244 as aut.show_storage() in a Jupyter notebook. See 1245 https://spot.lrde.epita.fr/ipynb/twagraph-internals.html 1246 1247 - spot::generic_emptiness_check() is a new function that performs 1248 emptiness checks of twa_graph_ptr (i.e., automata not built 1249 on-the-fly) with an *arbitrary* acceptance condition. Its sister 1250 spot::generic_emptiness_check_scc() can be used to decide the 1251 emptiness of an SCC. This is now used by 1252 twa_graph_ptr::is_empty(), twa_graph_ptr::intersects(), and 1253 scc_info::determine_unknown_acceptance(). 1254 1255 - The new function spot::to_parity() translates an automaton with 1256 arbitrary acceptance condition into a parity automaton, based on a 1257 last-appearance record (LAR) construction. (It is used by ltlsynt 1258 but not yet by autfilt or ltl2tgba.) 1259 1260 - The new function is_liveness() and is_liveness_automaton() can be 1261 used to check whether a formula or an automaton represents a 1262 liveness property. 1263 1264 - Two new functions count_univbranch_states() and 1265 count_univbranch_edges() can help measuring the amount of 1266 universal branching in alternating automata. 1267 1268 Bugs fixed: 1269 1270 - translate() would incorrectly mark as stutter-invariant 1271 some automata produced from formulas of the form X(f...) 1272 where f... is syntactically stutter-invariant. 1273 1274 - acc_cond::is_generalized_rabin() and 1275 acc_cond::is_generalized_streett() did not recognize the cases 1276 where a single generalized pair is used. 1277 1278 - The pair of acc_cond::mark_t returned by 1279 acc_code::used_inf_fin_sets(), and the pair (bool, 1280 vector_rs_pairs) by acc_cond::is_rabin_like() and 1281 acc_cond::is_streett_like() were not usable in Python. 1282 1283 - Many object types had __repr__() methods that would return the 1284 same string as __str__(), contrary to Python usage where repr(x) 1285 should try to show how to rebuild x. The following types have 1286 been changed to follow this convention: 1287 spot.acc_code 1288 spot.acc_cond 1289 spot.atomic_prop_set 1290 spot.formula 1291 spot.mark_t 1292 spot.twa_run (__repr__ shows type and address) 1293 spot.twa_word (likewise, but _repr_latex_ used in notebooks) 1294 1295 Note that this you were relying on the fact that Jupyter calls 1296 repr() to display returned values, you may want to call print() 1297 explicitly if you prefer the old representation. 1298 1299 - Fix compilation under Cygwin and Alpine Linux, both choking 1300 on undefined secure_getenv(). 1301 1302New in spot 2.6.3 (2018-10-17) 1303 1304 Bugs fixed: 1305 1306 - Running "ltl2tgba -B" on formulas of the type FG(safety) would 1307 unexpectedly use a co-Büchi automaton as an intermediate step. 1308 This in turn caused "ltl2tgba -U -B" to not produce unambiguous 1309 automata. 1310 1311 - ltl2tgba --low now disables the "gf-guarantee" feature, as 1312 documented. 1313 1314 - ltlfilt's --accept-word and --reject-word options were ignored 1315 unless used together. 1316 1317New in spot 2.6.2 (2018-09-28) 1318 1319 Build: 1320 1321 - We no longer distribute the Python-based CGI script + javascript 1322 code for the online translator. Its replacement has its own 1323 repository: https://gitlab.lrde.epita.fr/spot/spot-web-app/ 1324 1325 Library: 1326 1327 - When states are highlighted with more than 8 colors, print_dot() 1328 will add some extra markers to help distinguishing the colors. 1329 This helps with the fact that colors 8-15 are lighter versions of 1330 colors 0-7, and that higher color numbers cycle into this 16-color 1331 palette. 1332 1333 Bugs fixed: 1334 1335 - exclusive_ap::constrain() (called by autfilt --exclusive-ap=...) 1336 would incorrectly copy the "universal" property of the input 1337 automaton, causing print_hoa() to fail. 1338 1339 - configure --disable-doxygen would actually enable it. 1340 1341 - Fix several warnings emitted by the development version of GCC. 1342 1343New in spot 2.6.1 (2018-08-04) 1344 1345 Command-line tools: 1346 1347 - "ltlfilt --suspendable" is now a synonym for 1348 "ltlfilt --universal --eventual". 1349 1350 Bugs fixed: 1351 1352 - scc_info::split_on_sets() did not correctly register the 1353 atomic propositions of the returned automata. 1354 1355 - The spot::tl_simplifier class could raise an exception while 1356 attempting to reduce formulas containing unsimplified <->, -> or 1357 xor, if options nenoform_stop_on_boolean and synt_impl are both 1358 set. (This combination of options is not available from 1359 command-line tools.) 1360 1361 - The spot::contains(a, b) function introduced in 2.6 was testing 1362 a⊆b instead of a⊇b as one would expect. Unfortunately the 1363 documentation was also matching the code, so this is a backward 1364 incompatible change, but a short-lived one. 1365 1366 - The Python binding of the getter of spot::parsed_formula::f was 1367 returning a reference instead of a copy, causing issues if the 1368 reference outlasted the parsed_formula struct. 1369 1370 1371New in spot 2.6 (2018-07-04) 1372 1373 Command-line tools: 1374 1375 - autfilt learned --is-colored to filter automata that use 1376 exactly one acceptance set per mark or transition. 1377 1378 - autfilt learned --has-univ-branching and --has-exist-branching 1379 to keep automata that have universal branching, or that make 1380 non-deterministic choices. 1381 1382 - autcross' tool specifications now have %M replaced by the name of 1383 the input automaton. 1384 1385 - autcross now aborts if there is any parser diagnostic for the 1386 input automata (previous versions would use the input automaton 1387 whenever the parser would manage to read something). 1388 1389 - ltlcross, ltldo, and autcross learned shorthands to call 1390 delag, ltl2dra, ltl2dgra, and nba2dpa. 1391 1392 - When autfilt is asked to build a Büchi automaton from 1393 of a chain of many products, as in 1394 "autfilt -B --product 1.hoa ... --product n.hoa in.hoa" 1395 then it will automatically degeneralize the intermediate 1396 products to avoid exceeding the number of supported 1397 acceptance sets. 1398 1399 - genltl learned to generate six new families of LTL formulas: 1400 --gf-equiv-xn=RANGE GF(a <-> X^n(a)) 1401 --gf-implies-xn=RANGE GF(a -> X^n(a)) 1402 --sejk-f=RANGE[,RANGE] f(0,j)=(GFa0 U X^j(b)), f(i,j)=(GFai U 1403 G(f(i-1,j))) 1404 --sejk-j=RANGE (GFa1&...&GFan) -> (GFb1&...&GFbn) 1405 --sejk-k=RANGE (GFa1|FGb1)&...&(GFan|FGbn) 1406 --sejk-patterns[=RANGE] φ₁,φ₂,φ₃ from Sikert et al's [CAV'16] 1407 paper (range should be included in 1..3) 1408 1409 - genltl --ms-example can now take a two-range argument, 1410 (as --sejk-f above). 1411 1412 Build: 1413 1414 - ./configure --enable-max-accsets=N let you specify a maximum 1415 number of acceptance sets that Spot should support. The default 1416 is still 32, but this limit is no longer hard-coded. Larger values 1417 will cost additional memory and time. 1418 1419 - We know distribute RPM packages for Fedora 28. See 1420 file:///home/adl/git/spot/doc/userdoc/install.html#Fedora 1421 1422 Library: 1423 1424 - The PSL/LTL simplification routine learned the following: 1425 1426 q R Xf = X(q R f) if q is suspendable 1427 q U Xf = X(q U f) if q is suspendable 1428 {SERE;1} = {1} if {SERE} accepts [*0] 1429 {SERE;1} = {SERE} if {SERE} does not accept [*0] 1430 1431 - gf_guarantee_to_ba() is a specialized construction for translating 1432 formulas of the form GF(guarantee) to BA or DBA, and 1433 fg_safety_to_dca() is a specialized construction for translating 1434 formulas of the form FG(safety) to DCA. These are generalizations 1435 of some constructions proposed by J. Esparza, J. Křentínský, and 1436 S. Sickert (LICS'18). 1437 1438 These are now used by the main translation routine, and can be 1439 disabled by passing -x '!gf-guarantee' to ltl2tgba. For example, 1440 here are the size of deterministic transition-based generalized 1441 Büchi automata constructed from four GF(guarantee) formulas with 1442 two versions of Spot, and converted to other types of 1443 deterministic automata by other tools distributed with Owl 18.06. 1444 "x(y)" means x states and y acceptance sets. 1445 1446 ltl2tgba -D delag ltl2dra 1447 2.5 2.6 18.06 18.06 1448 ------------------------- ----------- ------------- 1449 GF(a <-> XXa) 9(1) 4(1) 4(2) 9(4) 1450 GF(a <-> XXXa) 27(1) 8(1) 8(2) 25(4) 1451 GF(((a & Xb) | XXc) & Xd) 6(1) 4(1) 16(1) 5(2) 1452 GF((b | Fa) & (b R Xb)) 6(2) 2(1) 3(4) 3(4) 1453 1454 Note that in the above the automata produced by 'ltl2tgba -D' in 1455 version 2.5 were not deterministic (because -D is only a 1456 preference). They are deterministic in 2.6 and other tools. 1457 1458 - spot::product() and spot::product_or() learned to produce an 1459 automaton with a simpler acceptance condition if one of the 1460 argument is a weak automaton. In this case the resulting 1461 acceptance condition is (usually) that of the other argument. 1462 1463 - spot::product_susp() and spot::product_or_susp() are new 1464 functions for building products between an automaton A and 1465 a "suspendable" automaton B. They are also optimized for 1466 the case that A is weak. 1467 1468 - When 'generic' acceptance is enabled, the translation routine will 1469 split the input formula on Boolean operators into components that 1470 are syntactically 'obligation', 'suspendable', or 'something 1471 else'. Those will be translated separately and combined with 1472 product()/product_susp(). This is inspired by the ways things are 1473 done in ltl2dstar or delag, and can be disabled by passing option 1474 -xltl-split=0, as in ltl2tgba -G -D -xltl-split=0. Here are the 1475 sizes of deterministic automata (except for ltl3tela which produces 1476 non-deterministic automata) produced with generic acceptance 1477 using two versions of ltl2tgba and other tools for reference. 1478 1479 ltl2tgba -DG delag ltl3tela 1480 2.5 2.6 18.06 1.1.2 1481 ------------ ------- -------- 1482 FGa0&GFb0 2(2) 1(2) 1(2) 1(2) 1483 (FGa1&GFb1)|FGa0|GFb0 16(6) 1(4) 1(4) 1(9) 1484 (FGa2&GFb2)|((FGa1|GFb1)&FGa0&GFb0) 29(8) 1(6) 1(6) 3(11) 1485 FGa0|GFb0 5(4) 1(2) 1(2) 1(5) 1486 (FGa1|GFb1)&FGa0&GFb0 8(4) 1(4) 1(4) 1(7) 1487 (FGa2|GFb2)&((FGa1&GFb1)|FGa0|GFb0) 497(14) 1(6) 1(6) 1(14) 1488 GFa1 <-> GFz 4(6) 1(3) 1(4) 1(7) 1489 (GFa1 & GFa2) <-> GFz 8(4) 1(3) 1(6) 3(10) 1490 (GFa1 & GFa2 & GFa3) <-> GFz 21(4) 1(4) 1(8) 3(13) 1491 GFa1 -> GFz 5(4) 1(2) 1(2) 1(5) 1492 (GFa1 & GFa2) -> GFz 12(4) 1(3) 1(3) 1(6) 1493 (GFa1 & GFa2 & GFa3) -> GFz 41(4) 1(4) 1(4) 1(7) 1494 FG(a|b)|FG(!a|Xb) 4(2) 2(2) 2(2) 2(3) 1495 FG(a|b)|FG(!a|Xb)|FG(a|XXb) 21(2) 4(3) 4(3) 4(4) 1496 FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb) 170(2) 8(4) 8(4) 8(5) 1497 1498 - For 'parity' output, the 'ltl-split' optimization just separates 1499 obligation sub-formulas from the rest, where a determinization is 1500 still performed. 1501 ltl2tgba -DP ltl3dra ltl2dpa 1502 2.5 2.6 0.2.3 18.06 1503 -------------- ------- ------- 1504 FGp0 & (Gp1 | XFp2) 6(2) 4(1) 4(1) 4(2) 1505 G!p0 | F(p0 & (!p1 W p2)) 5(2) 4(2) n/a 5(2) 1506 (p0 W XXGp0) & GFp1 & FGp2 6(2) 5(2) n/a 6(3) 1507 1508 (The above just show a few cases that were improved. There are 1509 many cases where ltl2dpa still produces smaller automata.) 1510 1511 - The automaton postprocessor will now simplify acceptance 1512 conditions more aggressively, calling spot::simplify_acceptance() 1513 or spot::cleanup_acceptance() depending on the optimization level. 1514 1515 - print_dot(), used to print automata in GraphViz's format, 1516 underwent several changes: 1517 1518 * option "a", for printing the acceptance condition, is now 1519 enabled by default. Option "A", introduced in Spot 2.4, can be 1520 used to hide the acceptance condition in case you do not want 1521 it. This change of course affects the --dot option of all the 1522 command-line tools, as well as the various way to display 1523 automata using the Python bindings. 1524 1525 * when option "1" is used to hide state names and force the 1526 display of state numbers, the actual state names is now moved to 1527 the "tooltip" field of the state. The SVG files produced by 1528 "dot -Tsvg" will show those as popups. This is also done for 1529 state labels of Kripke structures. 1530 1531 * the output digraph is now named using the name of the automaton 1532 if available, or the empty string otherwise. (Previous versions 1533 used to call all digraphs "G".) This name appears as a tooltip 1534 in SVG figures when the mouse is over the acceptance condition. 1535 1536 * a new option "u" hides "true states" behind "exiting 1537 transitions". This can be used to display alternating automata 1538 in a way many people expect. 1539 1540 * a new option "K" cancels the effect of "k" (which uses state 1541 labels whenever possible). This is most useful when one want to 1542 force transition-labeling of a Kripke structure, where "k" is 1543 usually the default. 1544 1545 - spot::twa_graph::merge_states() is a new method that merges states 1546 with the exact same outgoing edges. As it performs no reordering 1547 of the edges, it is better to call it when you know that the edges 1548 in the twa_graph are sorted (e.g. after a call to merge_edges()). 1549 1550 - spot::twa_graph::purge_unreachable_states() now takes a function 1551 which is called with the new numbering of states. This is useful 1552 to update an external structure that references states of the twa 1553 that we want to purge. 1554 1555 - spot::scc_filter() now automatically turns automata marked as 1556 inherently-weak into weak automata with state-based acceptance. 1557 The acceptance condition is set to Büchi unless the input had 1558 co-Büchi or t acceptance. spot::scc_filter_states() will pass 1559 inherently-weak automata to spot::scc_filter(). 1560 1561 - spot::cleanup_parity() and spot::cleanup_parity_here() are smarter 1562 and now remove from the acceptance condition the parity colors 1563 that are not used in the automaton. 1564 1565 - spot::contains() and spot::are_equivalent() can be used to 1566 check language containment between two automata or formulas. 1567 They are most welcome in Python, since we used to redefine 1568 them every now and them. Some examples are shown in 1569 https://spot.lrde.epita.fr/ipynb/contains.html 1570 1571 - aut1->exclusive_word(aut2) is a new method that returns a word 1572 accepted by aut1 or aut2 but not both. The exclusive_run() 1573 variant will return. This is useful when comparing automata and 1574 looking for differences. See also 1575 https://spot.lrde.epita.fr/ipynb/contains.html 1576 1577 - spot::complement_semidet(aut) is a new function that returns the 1578 complement of aut, where aut is a semi-deterministic automaton. The 1579 function uses the NCSB complementation algorithm proposed by 1580 F. Blahoudek, M. Heizmann, S. Schewe, J. Strejček, and MH. Tsai 1581 (TACAS'16). 1582 1583 - spot::remove_alternation() was slightly improved on very-weak 1584 alternating automata: the labeling of the outgoing transitions in 1585 the resulting TGBA makes it more likely that simulation-based 1586 reductions will reduce it. 1587 1588 - When applied to automata that are not WDBA-realizable, 1589 spot::minimize_wdba() was changed to produce an automaton 1590 recognizing a language that includes the original one. As a 1591 consequence spot::minimize_obligation() and 1592 spot::is_wdba_realizable() now only need one containment check 1593 instead of two. 1594 1595 - Slightly improved log output for the SAT-based minimization 1596 functions. The CSV log files now include an additional column 1597 with the size of the reference automaton, and they now have a 1598 header line. These log files give more details and are more 1599 accurate in the case of incremental SAT-solving. 1600 1601 Python: 1602 1603 - New spot.jupyter package. This currently contains a function for 1604 displaying several arguments side by side in a Jupyter notebook. 1605 See https://spot.lrde.epita.fr/ipynb/alternation.html for some 1606 examples. 1607 1608 - Strings are now implicitly converted into formulas when passed 1609 as arguments to functions that expect formulas. Previously this 1610 was done only for a few functions. 1611 1612 - The Python bindings for sat_minimize() now have display_log and 1613 return_log options; these are demonstrated on the new 1614 https://spot.lrde.epita.fr/ipynb/satmin.html page. 1615 1616 Bugs fixed: 1617 1618 - Python *.py and *.so files are now always installed into the same 1619 directory. This was an issue on systems like Fedora that separate 1620 platform-specific packages from non-platform-specific ones. 1621 1622 - print_dot() will correctly escape strings containing \n in HTML 1623 mode. 1624 1625 - The HOA parser will now accept Alias: declarations that occur 1626 before AP:. 1627 1628 - The option --allow-dups of randltl now works properly. 1629 1630 - Converting generalized-co-Büchi to Streett using dnf_to_nca() 1631 could produce bogus automata if the input had rejecting SCCs. 1632 1633 Deprecation notices: 1634 1635 - The type spot::acc_cond::mark_t has been overhauled and uses 1636 a custom bit-vector to represent acceptance sets instead of 1637 storing everything in a "unsigned int". This change is 1638 to accommodate configure's --enable-max-accsets=N option and 1639 has several effect: 1640 1641 * The following shortcuts are deprecated: 1642 acc_cond::mark_t m1 = 0U; 1643 acc_cond::mark_t m2 = -1U; 1644 instead, use: 1645 acc_cond::mark_t m1 = {}; 1646 acc_cond::mark_t m2 = acc_cond::mark_t::all(); 1647 1648 * acc_cond::mark_t::value_t is deprecated. It is now only 1649 defined when --enable-max-accsets=32 (the default) and 1650 equal to "unsigned" for backward compatibility reasons. 1651 1652 Backward incompatibilities: 1653 1654 - Functions spot::parity_product() and spot::parity_product_or() 1655 were removed. The code was unused, hard to maintain, and bogus. 1656 1657 - The output of print_dot() now include the acceptance condition. 1658 Add option "A" (supported since version 2.4) to cancel that. 1659 1660 - Because genltl now supports LTL pattern with two arguments, using 1661 --format=%L may output two comma-separated integer. This is an 1662 issue if you used to produce CSV files using for instance: 1663 genltl --format='%F,%L,%f' ... 1664 Make sure to quote %L to protect the potential commas: 1665 genltl --format='%F,"%L",%f' ... 1666 1667 - In Spot 2.5 and prior running "ltl2tgba --generic --det" on some 1668 formula would attempt to translate it as deterministic TGBA or 1669 determinize it into an automaton with parity acceptance. Version 1670 2.5 introduced --parity to force parity acceptance on the output. 1671 This version finally gives --generic some more natural semantics: 1672 any acceptance condition can be used. 1673 1674 1675New in spot 2.5.3 (2018-04-20) 1676 1677 Bugs fixed: 1678 1679 - "autfilt --cobuchi --small/--det" would turn a transition-based 1680 co-Büchi automaton into a state-based co-Büchi. 1681 1682 - Fix cryptic error message from Python's spot.translate() and 1683 spot.postprocess() when supplying conflicting arguments. 1684 1685 - "autfilt -B --sat-minimize" was incorrectly producing 1686 transition-based automata. 1687 1688 - Using spot.automata("cmd...|") to read just a few automata out of 1689 an infinite stream would not properly terminate the command. 1690 1691 - The is_unambiguous() check (rewritten in Spot 2.2) could mark some 1692 unambiguous automata as ambiguous. 1693 1694New in spot 2.5.2 (2018-03-25) 1695 1696 Bugs fixed: 1697 1698 - acc_cond::is_generalized_rabin() and 1699 acc_cond::is_generalized_streett() would segfault on weird 1700 acceptance conditions such as "3 t" or "3 f". 1701 1702 - remove_fin() and streett_to_generalized_buchi() should never 1703 return automata with "f" acceptance. 1704 1705 - "autfilt --acceptance-is=Fin-less" no longer accept automata 1706 with "f" acceptance. 1707 1708 - twa_run methods will now diagnose cases where the cycle is 1709 unexpectedly empty instead of segfaulting. 1710 1711 - spot::closure(), used by default for testing stutter-invariance, 1712 was using an optimization incorrect if the acceptance condition 1713 had some Fin(x). Consequently stutter-invariance tests for 1714 automata, for instance with "autfilt --is-stutter-invariant", 1715 could be to be wrong (even if the input does not use Fin(x), its 1716 complement, used in the stutter-invariance test likely will). 1717 Stutter-invariance checks of LTL formulas are not affected. 1718 1719New in spot 2.5.1 (2018-02-20) 1720 1721 Library: 1722 1723 - iar() and iar_maybe() now also handle Streett-like conditions. 1724 1725 Bugs fixed: 1726 1727 - iar() and iar_maybe() properly handle Rabin-like conditions. 1728 1729 - streett_to_generalized_buchi() could produce incorrect result on 1730 Streett-like input with acceptance like (Inf(0)|Fin(1))&Fin(1) 1731 where some Fin(x) is used both with and without a paired Fin(y). 1732 1733 - is_generalized_rabin() had a typo that caused some non-simplified 1734 acceptance conditions like Fin(0)|(Fin(0)&Inf(1)) to be 1735 incorrectly detected as generalized-Rabin 2 0 1 and then output 1736 as Fin(0)|(Fin(1)&Inf(2)) instead. Likewise for 1737 is_generalized_streett 1738 1739 - the conversion from Rabin to Büchi was broken on Rabin-like 1740 acceptance condition where one pair used Fin(x) and another pair 1741 used Inf(x) with the same x. Unfortunately, this situation could 1742 also occur as a side effect of simplifying the acceptance 1743 condition (by merging identical set) of some automaton prior to 1744 converting it to Büchi. 1745 1746 - dnf_to_dca() was mishandling some Rabin-like input. 1747 1748New in spot 2.5 (2018-01-20) 1749 1750 Build: 1751 1752 - We no longer distribute the doxygen-generated documentation in 1753 the tarball of Spot to save space. This documentation is still 1754 available online at https://spot.lrde.epita.fr/doxygen/. If you 1755 want to build a local copy you can configure Spot with 1756 --enable-doxygen, or simply run "cd doc && make doc". 1757 1758 - All the images that illustrate the documentation have been 1759 converted to SVG, to save space and improve quality. 1760 1761 Tools: 1762 1763 - ltlsynt is a new tool for synthesizing a controller from LTL/PSL 1764 specifications. 1765 1766 - ltlcross learned --reference=COMMANDFMT to specify a translator 1767 that should be trusted. Doing so makes it possible to reduce the 1768 number of tests to be performed, as all other translators will be 1769 compared to the reference's output when available. Multiple 1770 reference can be given; in that case other tools are compared 1771 against the smallest reference automaton. 1772 1773 - autcross, ltlcross, and ltldo learned --fail-on-timeout. 1774 1775 - ltl2tgba, autfilt, and dstar2tgba have some new '--parity' and 1776 '--colored-parity' options to force parity acceptance on the 1777 output. Different styles can be requested using for instance 1778 --parity='min odd' or --parity='max even'. 1779 1780 - ltl2tgba, autfilt, and dstar2tgba have some new '--cobuchi' option 1781 to force co-Büchi acceptance on the output. Beware: if the input 1782 language is not co-Büchi realizable the output automaton will 1783 recognize a superset of the input. Currently, the output is 1784 always state-based. 1785 1786 - genltl learned to generate six new families of formulas, taken from 1787 the SYNTCOMP competition on reactive synthesis, and from from 1788 Müller & Sickert's GandALF'17 paper: 1789 --gf-equiv=RANGE (GFa1 & GFa2 & ... & GFan) <-> GFz 1790 --gf-implies=RANGE (GFa1 & GFa2 & ... & GFan) -> GFz 1791 --ms-example=RANGE GF(a1&X(a2&X(a3&...)))&F(b1&F(b2&F(b3&...))) 1792 --ms-phi-h=RANGE FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb)|... 1793 --ms-phi-r=RANGE (FGa{n}&GFb{n})|((FGa{n-1}|GFb{n-1})&(...)) 1794 --ms-phi-s=RANGE (FGa{n}|GFb{n})&((FGa{n-1}&GFb{n-1})|(...)) 1795 1796 - autfilt learned --streett-like to convert automata with DNF 1797 acceptance into automata with Streett-like acceptance. 1798 1799 - autfilt learned --acceptance-is=ACC to filter automata by 1800 acceptance condition. ACC can be the name of some acceptance 1801 class (e.g. Büchi, Fin-less, Streett-like) or a precise acceptance 1802 formula in the HOA syntax. 1803 1804 - ltldo learned to limit the number of automata it outputs using -n. 1805 1806 - ltlfilt learned to measure wall-time using --format=%r, and 1807 cpu-time with --format=%R. 1808 1809 - The --format=%g option of tools that output automata used to 1810 print the acceptance condition as a *formula* in the HOA format. 1811 This %g may now take optional arguments to print the acceptance 1812 *name* in different formats. For instance 1813 1814 ... | autfilt -o '%[s]g.hoa' 1815 1816 will separate a stream of automata into different files named 1817 by their acceptance name (Buchi, co-Buchi, Streett, etc.) or 1818 "other" if no name is known for the acceptance condition. 1819 1820 - Tools that produce formulas now support --format=%[OP]n to 1821 display the nesting depth of operator OP. 1822 1823 - The new -x tls-impl=N option allows to fine-tune the 1824 implication-based simplification rules of ltl2tgba. See the 1825 spot-x(7) man page for details. 1826 1827 - All tools learned to check the SPOT_OOM_ABORT environment 1828 variable. This is only useful for debuging out-of-memory 1829 conditions. See the spot-x(7) man page for details. 1830 1831 New functions in the library: 1832 1833 - spot::iar() and spot::iar_maybe() use index appearance records (IAR) 1834 to translate Rabin-like automata into equivalent parity automata. 1835 This translation preserves determinism and is especially useful when 1836 the input automaton is deterministic. 1837 1838 - spot::print_aiger() encodes an automaton as an AIGER circuit, as 1839 required by the SYNTCOMP competition. It relies on a new named 1840 property "synthesis outputs" that describes which atomic 1841 propositions are to be encoded as outputs of the circuits. 1842 1843 - spot::dnf_to_streett() converts any automaton with a DNF 1844 acceptance condition into a Streett-like automaton. 1845 1846 - spot::nsa_to_nca(), spot::dfn_to_nca(), spot::dfn_to_dca(), and 1847 spot::nsa_to_dca(), convert automata with DNF or Streett-like 1848 acceptance into deterministic or non-deterministic co-Büchi 1849 automata. spot::to_dca() and spot::to_nca() dispatch between 1850 these four functions. The language of produced automaton includes 1851 the original language, but may be larger if the original automaton 1852 is not co-Büchi realizable. Based on Boker & Kupferman FOSSACS'11 1853 paper. Currently only supports state-based output. 1854 1855 - spot::scc_info::states_on_acc_cycle_of() returns all states 1856 visited by any accepting cycle of the specified SCC. It only 1857 works on automata with Streett-like acceptance. 1858 1859 - spot::is_recurrence(), spot::is_persistence(), and 1860 spot::is_obligation() test if a formula is a recurrence, 1861 persistance or obligation. The SPOT_PR_CHECK and SPOT_O_CHECK 1862 environment variables can be used to select between multiple 1863 implementations of these functions (see the spot-x(7) man page). 1864 1865 - spot::is_colored() checks if an automaton is colored 1866 (i.e., every transition belongs to exactly one acceptance set). 1867 1868 - spot::change_parity() converts between different parity acceptance 1869 conditions. 1870 1871 - spot::colorize_parity() transforms an automaton with parity 1872 acceptance into a colored automaton (which is often what people 1873 working with parity automata expect). 1874 1875 - spot::cleanup_parity_acceptance() simplifies a parity acceptance 1876 condition. 1877 1878 - spot::parity_product() and spot::parity_product_or() are 1879 specialized (but expensive) products that preserve parity 1880 acceptance. 1881 1882 - spot::remove_univ_otf() removes universal transitions on the fly 1883 from an alternating Büchi automaton using Miyano and Hayashi's 1884 breakpoint algorithm. 1885 1886 - spot::stutter_invariant_states(), 1887 spot::stutter_invariant_letters(), 1888 spot::highlight_stutter_invariant_states(), ... These functions 1889 help study a stutter-sensitive automaton and detect the subset of 1890 states that are stutter-invariant. See 1891 https://spot.lrde.epita.fr/ipynb/stutter-inv.html for examples. 1892 1893 - spot::acc_cond::name(fmt) is a new method that names well-known 1894 acceptance conditions. The fmt parameter specifies the format to 1895 use for that name (e.g. to the style used in HOA, or that used by 1896 print_dot()). 1897 1898 - spot::formula::is_leaf() method can be used to detect formulas 1899 without children (atomic propositions, or constants). 1900 1901 - spot::nesting_depth() computes the nesting depth of any LTL 1902 operator. 1903 1904 - spot::check_determinism() sets both prop_semi_deterministic() 1905 and prop_universal() appropriately. 1906 1907 Improvements to existing functions in the library: 1908 1909 - spot::tgba_determinize() has been heavily rewritten and 1910 optimized. The algorithm has (almost) not changed, but it is 1911 much faster now. It also features an optimization for 1912 stutter-invariant automata that may produce slightly smaller 1913 automata. 1914 1915 - spot::scc_info now takes an optional argument to disable some 1916 features that are expensive and not always necessary. By 1917 default scc_info tracks the list of all states that belong to an 1918 SCC (you may now ask it not to), tracks the successor SCCs of 1919 each SCC (that can but turned off), and explores all SCCs of the 1920 automaton (you may request to stop on the first SCC that is 1921 found accepting). 1922 1923 - In some cases, spot::degeneralize() would output Büchi automata 1924 with more SCCs than its input. This was hard to notice, because 1925 very often simulation-based simplifications remove those extra 1926 SCCs. This situation is now detected by spot::degeneralized() 1927 and fixed before returning the automaton. A new optional 1928 argument can be passed to disable this behavior (or use -x 1929 degen-remscc=0 from the command-line). 1930 1931 - The functions for detecting stutter-invariant formulas or 1932 automata have been overhauled. Their interface changed 1933 slightly. They are now fully documented. 1934 1935 - spot::postprocessor::set_type() can now request different forms 1936 of parity acceptance as output. However currently the 1937 conversions are not very smart: if the input does not already 1938 have parity acceptance, it will simply be degeneralized or 1939 determinized. 1940 1941 - spot::postprocessor::set_type() can now request co-Büchi 1942 acceptance as output. This calls the aforementioned to_nca() or 1943 to_dca() functions. 1944 1945 - spot::remove_fin() will now call simplify_acceptance(), 1946 introduced in 2.4, before attempting its different Fin-removal 1947 strategies. 1948 1949 - spot::simplify_acceptance() was already merging identical 1950 acceptance sets, and detecting complementary sets i and j to 1951 perform the following simplifications 1952 Fin(i) & Inf(j) = Fin(i) 1953 Fin(i) | Inf(j) = Inf(i) 1954 It now additionally applies the following rules (again assuming i 1955 and j are complementary): 1956 Fin(i) & Fin(j) = f Inf(i) | Inf(j) = t 1957 Fin(i) & Inf(i) = f Fin(i) | Inf(i) = t 1958 1959 - spot::formula::map(fun) and spot::formula::traverse(fun) will 1960 accept additionnal arguments and pass them to fun(). See 1961 https://spot.lrde.epita.fr/tut03.html for some examples. 1962 1963 Python-specific changes: 1964 1965 - The "product-states" property of automata is now accessible via 1966 spot.twa.get_product_states() and spot.twa.set_product_states(). 1967 1968 - twa_word instances can be displayed as SVG pictures, with one 1969 signal per atomic proposition. For some examples, see the use of 1970 the show() method in https://spot.lrde.epita.fr/ipynb/word.html 1971 1972 - The test suite is now using v4 of the Jupyter Notebook format. 1973 1974 - The function rabin_is_buchi_realizable() as its name suggests checks 1975 if a rabin aut. is Büchi realizable. It is heavily based on 1976 tra_to_tba() algorithm. 1977 1978 Deprecation notices: 1979 1980 (These functions still work but compilers emit warnings.) 1981 1982 - spot::scc_info::used_acc(), spot::scc_info::used_acc_of() and 1983 spot::scc_info::acc() are deprecated. They have been renamed 1984 spot::scc_info::marks(), spot::scc_info::marks_of() and 1985 spot::scc_info::acc_sets_of() respectively for clarity. 1986 1987 Backward incompatible changes: 1988 1989 - The spot::closure(), spot::sl2(), spot::is_stutter_invariant() 1990 functions no longer take && arguments. The former two have 1991 spot::closure_inplace() and spot::sl2_inplace() variants. These 1992 functions also do not take a list of atomic propositions as an 1993 argument anymore. 1994 1995 - The spot::bmrand() and spot::prand() functions have been removed. 1996 They were not used at all in Spot, and it is not Spot's objective 1997 to provide such random functions. 1998 1999 - The spot::bdd_dict::register_all_propositions_of() function has 2000 been removed. This low-level function was not used anywhere in 2001 Spot anymore, since it's better to use spot::twa::copy_ap_of(). 2002 2003 Bugs fixed: 2004 2005 - spot::simplify_acceptance() could produce incorrect output if the 2006 first edge of the automaton was the only one with no acceptance 2007 set. In spot 2.4.x this function was only used by autfilt 2008 --simplify-acceptance; in 2.5 it is now used in remove_fin(). 2009 2010 - spot::streett_to_generalized_buchi() could generate incorrect 2011 automata with empty language if some Fin set did not intersect all 2012 accepting SCCs (in other words, the fix from 2.4.1 was incorrect). 2013 2014 - ltlcross could crash when calling remove_fin() on an automaton 2015 with 32 acceptance sets that would need an additional set. 2016 2017 - the down_cast() helper function used in severaly headers of Spot 2018 was not in the spot namespace, and caused issues with some 2019 configurations of GCC. 2020 2021New in spot 2.4.4 (2017-12-25) 2022 2023 Bugs fixed: 2024 2025 - The generic to_generalized_buchi() function would fail if the 2026 Fin-less & CNF version of the acceptance condition had several 2027 unit clauses. 2028 2029 - If the automaton passed to sbacc() was incomplete or 2030 non-deterministic because of some unreachable states, then it was 2031 possible that the output would marked similarly while it was in 2032 fact complete or deterministic. 2033 2034New in spot 2.4.3 (2017-12-19) 2035 2036 Bugs fixed: 2037 2038 - couvreur99_new() leaked memory when processing TωA that allocate 2039 states. 2040 2041 - Some mismatched placement-new/delete reported by ASAN were fixed. 2042 2043 - Static compilation was broken on MinGW. 2044 2045 - Execution of Jupyter notebooks from the testsuite failed with 2046 recent versions of Python. 2047 2048 - Fix some warnings triggered by the development version of g++. 2049 2050New in spot 2.4.2 (2017-11-07) 2051 2052 Tools: 2053 2054 - ltlcross and ltldo support ltl3tela, the new name of ltl3hoa. 2055 2056 Bugs fixed: 2057 2058 - Automata produced by "genaut --ks-nca=N" were incorrectly marked 2059 as not complete. 2060 2061 - Fix some cases for which the highest setting of formulas 2062 simplification would produce worse results than lower settings. 2063 2064New in spot 2.4.1 (2017-10-05) 2065 2066 Bugs fixed: 2067 2068 - The formula class failed to build {a->c[*]} although it is 2069 allowed by our grammar. 2070 2071 - spot::scc_info::determine_unknown_acceptance() incorrectly 2072 considered some rejecting SCC as accepting. 2073 2074 - spot::streett_to_generalized_buchi() could generate automata with 2075 empty language if some Fin set did not intersect all accepting 2076 SCCs. As a consequence, some Streett-like automata were 2077 considered empty even though they were not. Also, the same 2078 function could crash on input that had a Streett-like acceptance 2079 not using all declared sets. 2080 2081 - The twa_graph::merge_edges() function relied on BDD IDs to sort 2082 edges. This in turn caused some algorithms (like the 2083 degeneralization) to produce slighltly different (but still correct) 2084 outputs depending on the BDD operations performed before. 2085 2086 - spot::simulation() could incorrectly flag an automaton as 2087 non-deterministic. 2088 2089New in spot 2.4 (2017-09-06) 2090 2091 Build: 2092 2093 - Spot is now built in C++14 mode, so you need at least GCC 5 or 2094 clang 3.4. The current version of all major linux distributions 2095 ship with at least GCC 6, which defaults to C++14, so this should 2096 not be a problem. In *this* release of Spot, most of the header 2097 files are still C++11 compatible, so you should be able to include 2098 Spot in a C++11 project in case you do not yet want to upgrade. 2099 There is also an --enable-c++17 option to configure in case you 2100 want to force a build of Spot in C++17 mode. 2101 2102 Tools: 2103 2104 - genaut is a new binary that produces families of automata defined 2105 in the literature (in the same way as we have genltl for LTL 2106 formulas). 2107 2108 - autcross is a new binary that compares the output of tools 2109 transforming automata (in the same way as we have ltlcross for 2110 LTL translators). 2111 2112 - genltl learned two generate two new families of formulas: 2113 --fxg-or=RANGE F(p0 | XG(p1 | XG(p2 | ... XG(pn)))) 2114 --gxf-and=RANGE G(p0 & XF(p1 & XF(p2 & ... XF(pn)))) 2115 The later is a generalization of --eh-pattern=9, for which a 2116 single state TGBA always exists (but previous version of Spot 2117 would build larger automata). 2118 2119 - autfilt learned to build the union (--sum) or the intersection 2120 (--sum-and) of two languages by putting two automata side-by-side 2121 and fiddling with the initial states. This complements the already 2122 implemented intersection (--product) and union (--product-or), 2123 both based on a product. 2124 2125 - autfilt learned to complement any alternating automaton with 2126 option --dualize. (See spot::dualize() below.) 2127 2128 - autfilt learned --split-edges to convert labels that are Boolean 2129 formulas into labels that are min-terms. (See spot::split_edges() 2130 below.) 2131 2132 - autfilt learned --simplify-acceptance to simplify some acceptance 2133 conditions. (See spot::simplify_acceptance() below.) 2134 2135 - autfilt --decompote-strength has been renamed to --decompose-scc 2136 because it can now extract the subautomaton leading to an SCC 2137 specified by number. (The old name is still kept as an alias.) 2138 2139 - The --stats=%c option of tools producing automata can now be 2140 restricted to count complete SCCs, using %[c]c. 2141 2142 - Tools producing automata have a --stats=... option, and tools 2143 producing formulas have a --format=... option. These two options 2144 work similarly, the use of different names is just historical. 2145 Starting with this release, all tools that recognize one of these 2146 two options also accept the other one as an alias. 2147 2148 Library: 2149 2150 - A new library, libspotgen, gathers all functions used to generate 2151 families of automata or LTL formulas, used by genltl and genaut. 2152 2153 - spot::sum() and spot::sum_and() implements the union and the 2154 intersection of two automata by putting them side-by-side and 2155 using non-deterministim or universal branching on the initial 2156 state. 2157 2158 - twa objects have a new property: prop_complete(). This obviously 2159 acts as a cache for the is_complete() function. 2160 2161 - spot::dualize() complements any alternating automaton. Since 2162 the dual of a deterministic automaton is still deterministic, the 2163 function spot::dtwa_complement() has been deprecated and simply 2164 calls spot::dualize(). 2165 2166 - spot::decompose_strength() was extended and renamed to 2167 spot::decompose_scc() as it can now also extract a subautomaton 2168 leading to a particular SCC. A demonstration of this feature via 2169 the Python bindings can be found at 2170 https://spot.lrde.epita.fr/ipynb/decompose.html 2171 2172 - The print_dot() function will now display names for well known 2173 acceptance conditions under the formula when option 'a' is used. 2174 We plan to enable 'a' by default in a future release, so a new 2175 option 'A' has been added to hide the acceptance condition. 2176 2177 - The print_dot() function has a new experimental option 'x' to 2178 output labels are LaTeX formulas. This is meant to be used in 2179 conjunction with the dot2tex tool. See 2180 https://spot.lrde.epita.fr/oaut.html#dot2tex 2181 2182 - A new named property for automata called "original-states" can be 2183 used to record the origin of a state before transformation. It is 2184 currently defined by the degeneralization algorithms, and by 2185 transform_accessible() and algorithms based on it (like 2186 remove_ap::strip(), decompose_scc()). This is realy meant as an 2187 aid for writing algorithms that need this mapping, but it can also 2188 be used to debug these algorithms: the "original-states" 2189 information is displayed by the dot printer when the 'd' option is 2190 passed. For instance in 2191 2192 % ltl2tgba 'GF(a <-> Fb)' --dot=s 2193 % ltl2tgba 'GF(a <-> Fb)' | autfilt -B --dot=ds 2194 2195 the second command outputs an automaton with states that show 2196 references to the first one. 2197 2198 - A new named property for automata called "degen-levels" keeps track 2199 of the level of a state in a degeneralization. This information 2200 complements the one carried in "original-states". 2201 2202 - A new named property for automata called "simulated-states" can be 2203 used to record the origin of a state through simulation. The 2204 behavior is similar to "original-states" above. Determinization 2205 takes advantage of this in its pretty print. 2206 2207 - The new function spot::acc_cond::is_streett_like() checks whether 2208 an acceptance condition is conjunction of disjunctive clauses 2209 containing at most one Inf and at most one Fin. It builds a 2210 vector of pairs to use if we want to assume the automaton has 2211 Streett acceptance. The dual function is 2212 spot::acc_cond::is_rabin_like() works similarly. 2213 2214 - The degeneralize() function has learned to consider acceptance 2215 marks common to all edges comming to a state to select its initial 2216 level. A similar trick was already used in sbacc(), and saves a 2217 few states in some cases. 2218 2219 - There is a new spot::split_edges() function that transforms edges 2220 (labeled by Boolean formulas over atomic propositions) into 2221 transitions (labeled by conjunctions where each atomic proposition 2222 appear either positive or negative). This can be used to 2223 preprocess automata before feeding them to algorithms or tools 2224 that expect transitions labeled by letters. 2225 2226 - spot::scc_info has two new methods to easily iterate over the 2227 edges of an SCC: edges_of() and inner_edges_of(). 2228 2229 - spot::scc_info can now be passed a filter function to ignore 2230 or cut some edges. 2231 2232 - spot::scc_info now keeps track of acceptance sets that are common 2233 to all edges in an SCC. These can be retrieved using 2234 scc_info::common_sets_of(scc), and they are used by scc_info to 2235 classify some SCCs as rejecting more easily. 2236 2237 - The new function acc_code::remove() removes all the given 2238 acceptance sets from the acceptance condition. 2239 2240 - It is now possible to change an automaton acceptance condition 2241 directly by calling twa::set_acceptance(). 2242 2243 - spot::cleanup_acceptance_here now takes an additional boolean 2244 parameter specifying whether to strip useless marks from the 2245 automaton. This parameter is defaulted to true, in order to 2246 keep this modification backward-compatible. 2247 2248 - The new function spot::simplify_acceptance() is able to perform 2249 some simplifications on an acceptance condition, and might lead 2250 to the removal of some acceptance sets. 2251 2252 - The function spot::streett_to_generalized_buchi() is now able to 2253 work on automata with Streett-like acceptance. 2254 2255 - The function for converting deterministic Rabin automata to 2256 deterministic Büchi automata (when possible), internal to the 2257 remove_fin() procedure, has been updated to work with 2258 transition-based acceptance and with Rabin-like acceptance. 2259 2260 - spot::relabel_here() was used on automata to rename atomic 2261 propositions, it can now replace atomic propositions by Boolean 2262 subformula. This makes it possible to use relabeling maps 2263 produced by relabel_bse() on formulas. 2264 2265 - twa_graph::copy_state_names_from() can be used to copy the state 2266 names from another automaton, honoring "original-states" if 2267 present. 2268 2269 - Building automata for LTL formula with a large number N of atomic 2270 propositions can be costly, because several loops and 2271 data-structures are exponential in N. However a formula like 2272 ((a & b & c) | (d & e & f)) U ((d & e & f) | (g & h & i)) 2273 can be translated more efficiently by first building an automaton 2274 for (p0 | p1) U (p1 | p2), and then substituting p0, p1, p2 by the 2275 appropriate Boolean formula. Such a trick is now attempted 2276 for translation of formulas with 4 atomic propositions or 2277 more (this threshold can be changed, see -x relabel-bool=N in 2278 the spot-x(7) man page). 2279 2280 - The LTL simplification routines learned that an LTL formula like 2281 G(a & XF(b & XFc & Fd) can be simplified to G(a & Fb & Fc & Fd), 2282 and dually F(a | XG(b | XGc | Gd)) = F(a | Gb | Gc | Gd). 2283 2284 When working with SERE, the simplification of "expr[*0..1]" was 2285 improved. E.g. {{a[*]|b}[*0..1]} becomes {a[*]|b} instead of 2286 {{a[+]|b}[*0..1]}. 2287 2288 - The new function spot::to_weak_alternating() is able to take an 2289 input automaton with generalized Büchi/co-Büchi acceptance and 2290 convert it to a weak alternating automaton. 2291 2292 - spot::sbacc() is can now also convert alternating automata 2293 to state-based acceptance. 2294 2295 - spot::sbacc() and spot::degeneralize() learned to merge 2296 accepting sinks. 2297 2298 - If the SPOT_BDD_TRACE environment variable is set, statistics 2299 about BDD garbage collection and table resizing are shown. 2300 2301 - The & and | operators for acceptannce conditions have been changed 2302 slightly to be more symmetrical. In older versions, operator & 2303 would move Fin() terms to the front, but that is not the case 2304 anymore. Also operator & was already grouping all Inf() terms 2305 (for efficiency reasons), in this version operator | is 2306 symmetrically grouping all Fin() terms. 2307 2308 - The automaton parser is now reentrant, making it possible to 2309 process automata from different streams at the same time (i.e., 2310 using multiple spot::automaton_stream_parser instances at once). 2311 2312 - The print_hoa() and parse_automaton() functions have been updated 2313 to recognize the "exist-branch" property of the non-released HOA 2314 v1.1, as well as the new meaning of property "deterministic". (In 2315 HOA v1 "properties: deterministic" means that the automaton has no 2316 existential branching; in HOA v1.1 it disallows universal 2317 branching as well.) The meaning of "deterministic" in Spot has 2318 been adjusted to these new semantics, see "Backward-incompatible 2319 changes" below. 2320 2321 - The parser for HOA now recognizes and verifies correct use of the 2322 "univ-branch" property. This is known to be a problem with option 2323 -H1 of ltl3ba 1.1.2 and ltl3dra 0.2.4, so the environment variable 2324 SPOT_HOA_TOLERANT can be set to disable the diagnostic. 2325 2326 Python: 2327 2328 - The 'spot.gen' package exports the functions from libspotgen. 2329 See https://spot.lrde.epita.fr/ipynb/gen.html for examples. 2330 2331 Bugs fixed: 2332 2333 - When the remove_fin() function was called on some automaton with 2334 Inf-less acceptance involving at least one disjunction (e.g., 2335 generalized co-Büchi), it would sometimes output an automaton with 2336 transition-based acceptance but marked as state-based. 2337 2338 - The complete() function could complete an empty co-Büchi automaton 2339 into an automaton accepting everything. 2340 2341 Backward-incompatible changes: 2342 2343 - spot::acc_cond::mark_t::operator bool() has been marked as 2344 explicit. The implicit converion to bool (and, via bool, to int) 2345 was a source of bugs. 2346 2347 - spot::twa_graph::set_init_state(const state*) has been removed. 2348 It was never used. You always want to use 2349 spot::twa_graph::set_init_state(unsigned) in practice. 2350 2351 - The previous implementation of spot::is_deterministic() has been 2352 renamed to spot::is_universal(). The new version of 2353 spot::is_deterministic() requires the automaton to be both 2354 universal and existential. This should not make any difference in 2355 existing code unless you work with the recently added support for 2356 alternating automata. 2357 2358 - spot::acc_cond::mark_t::sets() now returns an internal iterable 2359 object instead of an std::vector<unsigned>. 2360 2361 - The color palette optionally used by print_dot() has been extended 2362 from 9 to 16 colors. While the first 8 colors are similar, they 2363 are a bit more saturated now. 2364 2365 deprecation notices: 2366 2367 (these functions still work but compilers emit warnings.) 2368 2369 - spot::decompose_strength() is deprecated, it has been renamed 2370 to spot::decompose_scc(). 2371 2372 - spot::dtwa_complement() is deprecated. prefer the more generic 2373 spot::dualize() instead. 2374 2375 - the spot::twa::prop_deterministic() methods have been renamed to 2376 spot::twa::prop_universal() for consistency with the change to 2377 is_deterministic() listed above. we have kept 2378 spot::twa::prop_deterministic() as a deprecated synonym for 2379 spot::twa::prop_universal() to help backward compatibility. 2380 2381 - the spot::copy() function is deprecated. use 2382 spot::make_twa_graph() instead. 2383 2384New in spot 2.3.5 (2017-06-22) 2385 2386 Bugs fixed: 2387 2388 - We have fixed new cases where translating multiple formulas in a 2389 single ltl2tgba run could produce automata different from those 2390 produced by individual runs. 2391 2392 - The print_dot() function had a couple of issues when printing 2393 alternating automata: in particular, when using flag 's' (display 2394 SCC) or 'y' (split universal destination by colors) universal 2395 edges could be connected to undefined states. 2396 2397 - Using --stats=%s or --stats=%s or --stats=%t could take an 2398 unnecessary long time on automata with many atomic propositions, 2399 due to a typo. Furthermore, %s/%e/%t/%E/%T were printing 2400 a number of reachable states/edges/transitions, but %S was 2401 incorrectly counting all states even unreachable. 2402 2403 - Our verson of BuDDy had an incorrect optimization for the 2404 biimp operator. 2405 2406New in spot 2.3.4 (2017-05-11) 2407 2408 Bugs fixed: 2409 2410 - The transformation to state-based acceptance (spot::sbacc()) was 2411 incorrect on automata where the empty acceptance mark is accepting. 2412 2413 - The --help output of randaut and ltl2tgba was showing an 2414 unsupported %b stat. 2415 2416 - ltldo and ltlcross could leave temporary files behind when 2417 aborting on error. 2418 2419 - The LTL simplifcation rule that turns F(f)|q into F(f|q) 2420 when q is a subformula that is both eventual and universal 2421 was documented but not applied in some forgotten cases. 2422 2423 - Because of some caching inside of ltl2tgba, translating multiple 2424 formula in single ltl2tgba run could produce automata different 2425 from those produced by individual runs. 2426 2427New in spot 2.3.3 (2017-04-11) 2428 2429 Tools: 2430 2431 - ltldo and ltlcross learned shorthands to talk to ltl2da, ltl2dpa, 2432 and ltl2ldba (from Owl) without needing to specify %f>%O. 2433 2434 - genltl learned --spec-patterns as an alias for --dac-patterns; it 2435 also learned two new sets of LTL formulas under --hkrss-patterns 2436 (a.k.a. --liberouter-patterns) and --p-patterns 2437 (a.k.a. --beem-patterns). 2438 2439 Bugs fixed: 2440 2441 - In "lenient" mode the formula parser would fail to recover from a 2442 missing closing brace. 2443 2444 - The output of 'genltl --r-left=1 --r-right=1 --format=%F' had 2445 typos. 2446 2447 - 'ltl2tgba Fa | autfilt --complement' would incorrectly claim that 2448 the output is "terminal" because dtwa_complement() failed to reset 2449 that property. 2450 2451 - spot::twa_graph::purge_unreachable_states() was misbehaving on 2452 alternating automata. 2453 2454 - In bench/stutter/ the .cc files were not compiling due to warnings 2455 being caught as errors. 2456 2457 - The code in charge of detecting DBA-type Rabin automata is 2458 actually written to handle a slightly larger class of acceptance 2459 conditions (e.g., Fin(0)|(Fin(1)&Inf(2))), however it failed to 2460 correctly detect DBA-typeness in some of these non-Rabin 2461 acceptance. 2462 2463New in spot 2.3.2 (2017-03-15) 2464 2465 Tools: 2466 2467 - In tools that output automata, the number of atomic propositions 2468 can be output using --stats=%x (output automaton) or --stats=%X 2469 (input automaton). Additional options can be passed to list 2470 atomic propositions instead of counting them. Tools that output 2471 formulas also support --format=%x for this purpose. 2472 2473 Python: 2474 2475 - The bdd_to_formula(), and to_generalized_buchi() functions can now 2476 be called in Python. 2477 2478 Documentation: 2479 2480 - https://spot.lrde.epita.fr/tut11.html is a new page describing 2481 how to build monitors in Shell, Python, or C++. 2482 2483 Bugs fixed: 2484 2485 - The tests using LTSmin's patched version of divine would fail 2486 if the current (non-patched) version of divine was installed. 2487 2488 - Because of a typo, the output of --stats='...%P...' was correct 2489 only if %p was used as well. 2490 2491 - genltl was never meant to have (randomly attributed) short 2492 options for --postive and --negative. 2493 2494 - a typo in the code for transformating transition-based acceptance 2495 to state-based acceptance could cause a superfluous initial state 2496 to be output in some cases (the result was still correct). 2497 2498 - 'ltl2tgba --any -C -M ...' would not complete automata. 2499 2500 - While not incorrect, the HOA properties output by 'ltl2tgba -M' 2501 could be 'inherently-weak' or 'terminal', while 'ltl2tgba -M -D' 2502 would always report 'weak' automata. Both variants now report the 2503 most precise between 'weak' or 'terminal'. 2504 2505 - spot::twa_graph::set_univ_init_state() could not be called with 2506 an initializer list. 2507 2508 - The Python wrappers for spot::twa_graph::state_from_number and 2509 spot::twa_graph::state_acc_sets were broken in 2.3. 2510 2511 - Instantiating an emptiness check on an automaton with unsupported 2512 acceptance condition should throw an exception. This used to be 2513 just an assertion, disabled in release builds; the difference 2514 matters for the Python bindings. 2515 2516 Deprecation notice: 2517 2518 - Using --format=%a to print the number of atomic propositions in 2519 ltlfilt, genltl, and randltl still works, but it is not documented 2520 anymore and should be replaced by the newly-introduced --format=%x 2521 for consistency with tools producing automata, where %a means 2522 something else. 2523 2524 2525New in spot 2.3.1 (2017-02-20) 2526 2527 Tools: 2528 2529 - ltldo learnt to act like a portfolio: --smallest and --greatest 2530 will select the best output automaton for each formula translated. 2531 See https://spot.lrde.epita.fr/ltldo.html#portfolio for examples. 2532 2533 - The colors used in the output of ltlcross have been adjusted to 2534 work better with white backgrounds and black backgrounds. 2535 2536 - The option (y) has been added to --dot. It splits the universal 2537 edges with the same targets but different colors. 2538 2539 - genltl learnt three new families for formulas: --kr-n2=RANGE, 2540 --kr-nlogn=RANGE, and --kr-n=RANGE. These formulas, from 2541 Kupferman & Rosenberg [MoChArt'10] are recognizable by 2542 deterministic Büchi automata with at least 2^2^n states. 2543 2544 Library: 2545 2546 - spot::twa_run::as_twa() has an option to preserve state names. 2547 2548 - the method spot::twa::is_alternating(), introduced in Spot 2.3 was 2549 badly named and has been deprecated. Use the negation of the new 2550 spot::twa::is_existential() instead. 2551 2552 Bugs fixed: 2553 2554 - spot::otf_product() was incorrectly registering atomic 2555 propositions. 2556 2557 - spot::ltsmin_model::kripke() forgot to register the "dead" 2558 proposition. 2559 2560 - The spot::acc_word type (used to construct acceptance condition) 2561 was using some non-standard anonymous struct. It is unlikely that 2562 this type was actually used outside Spot, but if you do use it, 2563 spot::acc_word::op and spot::acc_word::type had to be renamed as 2564 spot::acc_word::sub.op and spot::acc_word::sub.type. 2565 2566 - alternation_removal() was not always reporting the unsupported 2567 non-weak automata. 2568 2569 - a long-standing typo in the configure code checking for Python 2570 caused any user-defined CPPFLAGS to be ignored while building 2571 Spot. 2572 2573 - The display of clusters with universal edges was confused, because the 2574 intermediate node was not in the cluster even if one of the target was 2575 in the same one. 2576 2577New in spot 2.3 (2017-01-19) 2578 2579 Build: 2580 2581 * While Spot only relies on C++11 features, the configure script 2582 learned --enable-c++14 to compile in C++14 mode. This allows us 2583 check that nothing breaks when we will switch to C++14. 2584 2585 * Spot is now distributed with PicoSAT 965, and uses it for 2586 SAT-based minimization of automata without relying on temporary 2587 files. It is still possible to use an external SAT solver by 2588 setting the SPOT_SATSOLVER environment variable. 2589 2590 * The development Debian packages for Spot now install static 2591 libraries as well. 2592 2593 * We now install configuration files for users of pkg-config. 2594 2595 Tools: 2596 2597 * ltlcross supports translators that output alternating automata in 2598 the HOA format. Cross-comparison checks will only work with weak 2599 alternating automata (not necessarily *very* weak), but "ltlcross 2600 --no-check --product=0 --csv=..." will work with any alternating 2601 automaton if you just want satistics. 2602 2603 * autfilt can read alternating automata. This is still experimental 2604 (see below). Some of the algorithms proposed by autfilt will 2605 refuse to work because they have not yet been updated to work with 2606 alternating automata, but in any case they should display a 2607 diagnostic: if you see a crash, please report it. 2608 2609 * autfilt has three new filters: --is-very-weak, --is-alternating, 2610 and --is-semi-deterministic. 2611 2612 * the --check option of autfilt/ltl2tgba/ltldo/dstar2tgba can now 2613 take "semi-determinism" as argument. 2614 2615 * autfilt --highlight-languages will color states that recognize 2616 identical languages. (Only works for deterministic automata.) 2617 2618 * 'autfilt --sat-minimize' and 'ltl2tgba -x sat-minimize' have 2619 undergone some backward incompatible changes. They use binary 2620 search by default, and support different options than they used 2621 too. See spot-x(7) for details. The defaults are those that were 2622 best for the benchmark in bench/dtgbasat/. 2623 2624 * ltlfilt learned --recurrence and --persistence to match formulas 2625 belonging to these two classes of the temporal hierarchy. Unlike 2626 --syntactic-recurrence and --syntactic-persistence, the new checks 2627 are automata-based and will also match pathological formulas. 2628 See https://spot.lrde.epita.fr/hierarchy.html 2629 2630 * The --format option of ltlfilt/genltl/randltl/ltlgrind learned to 2631 print the class of a formula in the temporal hierarchy of Manna & 2632 Pnueli using %h. See https://spot.lrde.epita.fr/hierarchy.html 2633 2634 * ltldo and ltlcross learned a --relabel option to force the 2635 relabeling of atomic propositions to p0, p1, etc. This is more 2636 useful with ltldo, as it allows calling a tool that restricts the 2637 atomic propositions it supports, and the output automaton will 2638 then be fixed to use the original atomic propositions. 2639 2640 * ltldo and ltlcross have learned how to call ltl3hoa, so 2641 'ltl3hoa -f %f>%O' can be abbreviated to just 'ltl3hoa'. 2642 2643 Library: 2644 2645 * A twa is required to have at least one state, the initial state. 2646 An automaton can only be empty while it is being constructed, 2647 but should not be passed to other algorithms. 2648 2649 * Couvreur's emptiness check has been rewritten to use the explicit 2650 interface when possible, to avoid overkill memory allocations. 2651 The new version has further optimizations for weak and terminal 2652 automata. Overall, this new version is roughly 4x faster on 2653 explicit automata than the former one. The old version has been 2654 kept for backward compatibility, but will be removed eventually. 2655 2656 * The new version of the Couvreur emptiness check is now the default 2657 one, used by twa::is_empty() and twa::accepting_run(). Always 2658 prefer these functions over an explicit call to Couvreur. 2659 2660 * experimental support for alternating automata: 2661 2662 - twa_graph objects can now represent alternating automata. Use 2663 twa_graph::new_univ_edge() and twa_graph::set_univ_init_state() 2664 to create universal edges an initial states; and use 2665 twa_graph::univ_dests() to iterate over the universal 2666 destinations of an edge. 2667 2668 - the automaton parser will now read alternating automata in the 2669 HOA format. The HOA and dot printers can output them. 2670 2671 - the file twaalgos/alternation.hh contains a few algorithms 2672 specific to alternating automata: 2673 + remove_alternation() will transform *weak* alternating automata 2674 into TGBA. 2675 + the class outedge_combiner can be used to perform "and" and "or" 2676 on the outgoing edges of some alternating automaton. 2677 2678 - scc_info has been adjusted to handle universal edges as if they 2679 were existential edges. As a consequence, acceptance 2680 information is not accurate. 2681 2682 - postprocessor will call remove_alternation() right away, so 2683 it can be used as a way to transform alternating automata 2684 into different sub-types of (generalized) Büchi automata. 2685 Note that although prostprocessor optimize the resulting 2686 automata, it still has no simplification algorithms that work 2687 at the alternating automaton level. 2688 2689 - See https://spot.lrde.epita.fr/tut23.html 2690 https://spot.lrde.epita.fr/tut24.html and 2691 https://spot.lrde.epita.fr/tut31.html for some code examples. 2692 2693 * twa objects have two new properties, very-weak and 2694 semi-deterministic, that can be set or retrieved via 2695 twa::prop_very_weak()/twa::prop_semi_deterministic(), and that can 2696 be tested by is_very_weak_automaton()/is_semi_deterministic(). 2697 2698 * twa::prop_set has a new attribute used in twa::prop_copy() and 2699 twa::prop_keep() to indicate that determinism may be improved by 2700 an algorithm. In other words properties like 2701 deterministic/semi-deterministic/unambiguous should be preserved 2702 only if they are positive. 2703 2704 * language_map() and highlight_languages() are new functions that 2705 implement autfilt's --highlight-languages option mentionned above. 2706 2707 * dtgba_sat_minimize_dichotomy() and dwba_sat_minimize_dichotomy() 2708 use language_map() to estimate a lower bound for binary search. 2709 2710 * The encoding part of SAT-based minimization consumes less memory. 2711 2712 * SAT-based minimization of automata can now be done using two 2713 incremental techniques that take a solved minimization and attempt 2714 to forbid the use of some states. This is done either by adding 2715 clauses, or by using assumptions. 2716 2717 * If the environment variable "SPOT_XCNF" is set during incremental 2718 SAT-based minimization, XCNF files suitable for the incremental SAT 2719 competition will be generated. This requires the use of an exteral 2720 SAT solver, setup with "SPOT_SATSOLVER". See spot-x(7). 2721 2722 * The new function mp_class(f) returns the class of the formula 2723 f in the temporal hierarchy of Manna & Pnueli. 2724 2725Python: 2726 2727 * spot.show_mp_hierarchy() can be used to display the membership of 2728 a formula to the Manna & Pnueli hierarchy, in notebooks. An 2729 example is in https://spot.lrde.epita.fr/ipynb/formulas.html 2730 2731 * The on-line translator will now display the temporal hierarchy 2732 in the "Formula > property information" output. 2733 2734Bugs fixed: 2735 2736 * The minimize_wdba() function was not correctly minimizing automata 2737 with useless SCCs. This was not an issue for the LTL translation 2738 (where useless SCCs are always removed first), but it was an issue 2739 when deciding if a formula was safety or guarantee. As a 2740 consequence, some tricky safety or guarantee properties were only 2741 recognized as obligations. 2742 2743 * When ltlcross was running a translator taking the Spin syntax as 2744 input (%s) it would not automatically relabel any unsupported 2745 atomic propositions as ltldo already do. 2746 2747 * When running "autfilt --sat-minimize" on a automaton representing 2748 an obligation property, the result would always be a complete 2749 automaton even without the -C option. 2750 2751 * ltlcross --products=0 --csv should not output any product-related 2752 column in the CSV output since it has nothing to display there. 2753 2754New in spot 2.2.2 (2016-12-16) 2755 2756 Build: 2757 2758 * If the system has an installed libltdl library, use it instead of 2759 the one we distribute. 2760 2761 Bug fixes: 2762 2763 * scc_filter() had a left-over print statement that would print 2764 "names" when copying the name of the states. 2765 2766 * is_terminal() should reject automata that have accepting 2767 transitions going into rejecting SCCs. The whole point of 2768 being a terminal automaton is that reaching an accepting 2769 transition guarantees that any suffix will be accepted. 2770 2771 * The HOA parser incorrectly read "Acceptance: 1 Bar(0)" as a valid 2772 way to specify "Acceptance: 1 Fin(0)" because it assumed that 2773 everything that was not Inf was Fin. These errors are now 2774 diagnosed. 2775 2776 * Some of the installed headers (spot/misc/fixpool.hh, 2777 spot/misc/mspool.hh, spot/twaalgos/emptiness_stats.hh) were not 2778 self-contained. 2779 2780 * ltlfilt --from-ltlf should ensure that "alive" holds initially in 2781 order to reject empty traces. 2782 2783 * the on-line translator had a bug where a long ltl3ba process would 2784 continue running even after the script had timeout'ed. 2785 2786New in spot 2.2.1 (2016-11-21) 2787 2788 Bug fix: 2789 2790 * The bdd_noderesize() function, as modified in 2.2, would always 2791 crash. 2792 2793New in spot 2.2 (2016-11-14) 2794 2795 Command-line tools: 2796 2797 * ltlfilt has a new option --from-ltlf to help reducing LTLf (i.e., 2798 LTL over finite words) model checking to LTL model checking. This 2799 is based on a transformation by De Giacomo & Vardi (IJCAI'13). 2800 2801 * "ltldo --stats=%R", which used to display the serial number of the 2802 formula processed, was renamed to "ltldo --stats=%#" to free %R 2803 for the following feature. 2804 2805 * autfilt, dstar2tgba, ltl2tgba, ltlcross, ltldo learned to measure 2806 cpu-time (as opposed to wall-time) using --stats=%R. User or 2807 system time, for children or parent, can be measured separately by 2808 adding additional %[LETTER]R options. The difference between %r 2809 (wall-clock time) and %R (CPU time) can also be used to detect 2810 unreliable measurements. See 2811 https://spot.lrde.epita.fr/oaut.html#timing 2812 2813 Library: 2814 2815 * from_ltlf() is a new function implementing the --from-ltlf 2816 transformation described above. 2817 2818 * is_unambiguous() was rewritten in a more efficient way. 2819 2820 * scc_info learned to determine the acceptance of simple SCCs made 2821 of a single self-loop without resorting to remove_fin() for complex 2822 acceptance conditions. 2823 2824 * remove_fin() has been improved to better deal with automata with 2825 "unclean" acceptance, i.e., acceptance sets that are declared but 2826 not used. In particular, this helps scc_info to be more efficient 2827 at deciding the acceptance of SCCs in presence of Fin acceptance. 2828 2829 * Simulation-based reductions now implement just bisimulation-based 2830 reductions on deterministic automata, to save time. As an example, 2831 this halves the run time of 2832 genltl --rv-counter=10 | ltl2tgba 2833 2834 * scc_filter() learned to preserve state names and highlighted states. 2835 2836 * The BuDDy library has been slightly optimized: the initial setup 2837 of the unicity table can now be vectorized by GCC, and all calls 2838 to setjmp are now avoided when variable reordering is disabled 2839 (the default). 2840 2841 * The twa class has three new methods: 2842 aut->intersects(other) 2843 aut->intersecting_run(other) 2844 aut->intersecting_word(other) 2845 currently these are just convenient wrappers around 2846 !otf_product(aut, other)->is_empty() 2847 otf_product(aut, other)->accepting_run()->project(aut) 2848 otf_product(aut, other)->accepting_word() 2849 with any Fin-acceptance removal performed before the product. 2850 However the plan is to implement these more efficiently in the 2851 future. 2852 2853 Bug fixes: 2854 2855 * ltl2tgba was always using the highest settings for the LTL 2856 simplifier, ignoring the --low and --medium options. Now 2857 genltl --go-theta=12 | ltl2tgba --low --any 2858 is instantaneous as it should be. 2859 2860 * The int-vector compression code could encode 6 and 22 in the 2861 same way, causing inevitable issues in our LTSmin interface. 2862 (This affects tests/ltsmin/modelcheck with option -z, not -Z.) 2863 2864 * str_sere() and str_utf8_sere() were not returning the same 2865 string that print_sere() and print_utf8_sere() would print. 2866 2867 * Running the LTL parser in debug mode would crash. 2868 2869 * tgba_determinize() could produce incorrect deterministic automata 2870 when run with use_simulation=true (the default) on non-simplified 2871 automata. 2872 2873 * When the automaton_stream_parser reads an automaton from an 2874 already opened file descriptor, it will not close the file 2875 anymore. Before that the spot.automata() python function used to 2876 close a file descriptor twice when reading from a pipe, and this 2877 led to crashes of the 0MQ library used by Jupyter, killing the 2878 Python kernel. 2879 2880 * remove_fin() could produce incorrect result on incomplete 2881 automata tagged as weak and deterministic. 2882 2883 * calling set_acceptance() several times on an automaton could 2884 result in unexpected behaviors, because set_acceptance(0,...) 2885 used to set the state-based acceptance flag automatically. 2886 2887 * Some buffering issue caused syntax errors to be displayed out 2888 of place by the on-line translator. 2889 2890New in spot 2.1.2 (2016-10-14) 2891 2892 Command-line tools: 2893 2894 * genltl learned 5 new families of formulas 2895 (--tv-f1, --tv-f2, --tv-g1, --tv-g2, --tv-uu) 2896 defined in Tabakov & Vardi's RV'10 paper. 2897 2898 * ltlcross's --csv and --json output was changed to not include 2899 information about the ambiguity or strength of the automata by 2900 default. Computing those can be costly and not needed by 2901 every user, so it should now be requested explicitely using 2902 options --strength and --ambiguous. 2903 2904 Library: 2905 2906 * New LTL simplification rule: 2907 2908 - GF(f & q) = G(F(f) & q) if q is 2909 purely universal and a pure eventuality. In particular 2910 GF(f & GF(g)) now ultimately simplifies to G(F(f) & F(g)). 2911 2912 Bug fixes: 2913 2914 * Fix spurious uninitialized read reported by valgrind when 2915 is_Kleene_star() is compiled by clang++. 2916 2917 * Using "ltlfilt some-large-file --some-costly-filter" could take 2918 to a lot of time before displaying the first results, because the 2919 output of ltlfilt is buffered: the buffer had to fill up before 2920 being flushed. The issue did not manifest when the input is 2921 standard input, because of the C++ feature that reading std::cin 2922 should flush std::cout; however it was well visible when reading 2923 from files. Flushing is now done more regularly. 2924 2925 * Fix compilation warnings when -Wimplicit-fallthrough it enabled. 2926 2927 * Fix python errors on Darwin when using methods from the spot module 2928 inside of the spot.ltsmin submodule. 2929 2930 * Fix ltlcross crash when combining --no-check with --verbose. 2931 2932 * Adjust paths and options used in bench/dtgbasat/ to match the 2933 changes introduced in Spot 2.0. 2934 2935New in spot 2.1.1 (2016-09-20) 2936 2937 Command-line tools: 2938 2939 * ltlfilt, randltl, genltl, and ltlgrind learned to display the size 2940 (%s), Boolean size (%b), and number of atomic propositions (%a) 2941 with the --format and --output options. A typical use-case is to 2942 sort formulas by size: 2943 genltl --dac --format='%s,%f' | sort -n | cut -d, -f2 2944 or to group formulas by number of atomic propositions: 2945 genltl --dac --output='ap-%a.ltl' 2946 2947 * autfilt --stats learned the missing %D, %N, %P, and %W sequences, 2948 to complete the existing %d, %n, %p, and %w. 2949 2950 * The --stats %c option of ltl2tgba, autfilt, ltldo, and dstar2tgba 2951 now accepts options to filter the SCCs to count. For instance 2952 --stats='%[awT]c' will count the SCCs that are (a)ccepting and 2953 (w)eak, but (not t)erminal. See --help for all supported filters. 2954 2955 Bugs fixed: 2956 2957 * Fix several cases where command-line tools would fail to diagnose 2958 write errors (e.g. when writing to a filesystem that is full). 2959 * Typos in genltl --help and in the man page spot-x(7). 2960 2961New in spot 2.1 (2016-08-08) 2962 2963 Command-line tools: 2964 2965 * All tools that input formulas or automata (i.e., autfilt, 2966 dstar2tgba, ltl2tgba, ltl2tgta, ltlcross, ltldo, ltlfilt, 2967 ltlgrind) now have a more homogeneous handling of the default 2968 input. 2969 2970 - If no formula/automaton have been specified, and the standard 2971 input is a not a tty, then the default is to read that. This is a 2972 change for ltl2tgba and ltl2tgta. In particular, it simplifies 2973 2974 genltl --dac | ltl2tgba -F- | autfilt ... 2975 2976 into 2977 2978 genltl --dac | ltl2tgba | autfilt ... 2979 2980 - If standard input is a tty and no other input has been 2981 specified, then an error message is printed. This is a change for 2982 autfilt, dstar2tgba, ltlcross, ltldo, ltlfilt, ltlgrind, that used 2983 to expect the user to type formula or automata at the terminal, 2984 confusing people. 2985 2986 - All tools now accept - as a shorthand for -F-, to force reading 2987 input from the standard input (regardless of whether it is a tty 2988 or not). This is a change for ltl2tgba, ltl2tgta, ltlcross, and 2989 ltldo. 2990 2991 * ltldo has a new option --errors=... to specify how to deal 2992 with errors from executed tools. 2993 2994 * ltlcross and ltldo learned to bypass the shell when executing 2995 simple commands (with support for single or double-quoted 2996 arguments, and redirection of stdin and stdout, but nothing more). 2997 2998 * ltlcross and ltldo learned a new syntax to specify that an input 2999 formula should be written in some given syntax after rewriting 3000 some operators away. For instance the defaults arguments passed 3001 to ltl2dstar have been changed from 3002 --output-format=hoa %L %O 3003 into 3004 --output-format=hoa %[WM]L %O 3005 where [WM] specifies that operators W and M should be rewritten 3006 away. As a consequence running 3007 ltldo ltl2dstar -f 'a M b' 3008 will now work and call ltl2dstar on the equivalent formula 3009 'b U (a & b)' instead. The operators that can be listed between 3010 brackets are the same as those of ltlfilt --unabbreviate option. 3011 3012 * ltlcross learned to show some counterexamples when diagnosing 3013 failures of cross-comparison checks against random state spaces. 3014 3015 * autfilt learned to filter automata by count of SCCs (--sccs=RANGE) 3016 or by type of SCCs (--accepting-sccs=RANGE, 3017 --rejecting-sccs=RANGE, trivial-sccs=RANGE, --terminal-sccs=RANGE, 3018 --weak-sccs=RANGE, --inherently-weak-sccs=RANGE). 3019 3020 * autfilt learned --remove-unused-ap to remove atomic propositions 3021 that are declared in the input automaton, but not actually used. 3022 This of course makes sense only for input/output formats that 3023 declare atomic propositions (HOA & DSTAR). 3024 3025 * autfilt learned two options to filter automata by count of used or 3026 unused atomic propositions: --used-ap=RANGE --unused-ap=RANGE. 3027 These differ from --ap=RANGE that only consider *declared* atomic 3028 propositions, regardless of whether they are actually used. 3029 3030 * autfilt learned to filter automata by count of nondeterministsic 3031 states with --nondet-states=RANGE. 3032 3033 * autfilt learned to filter automata representing stutter-invariant 3034 properties with --is-stutter-invariant. 3035 3036 * autfilt learned two new options to highlight non-determinism: 3037 --highlight-nondet-states=NUM and --highlight-nondet-states=NUM 3038 where NUM is a color number. Additionally --highlight-nondet=NUM is 3039 a shorthand for using the two. 3040 3041 * autfilt learned to highlight a run matching a given word using the 3042 --highlight-word=[NUM,]WORD option. However currently this only 3043 work on automata with Fin-less acceptance. 3044 3045 * autfilt learned two options --generalized-rabin and 3046 --generalized-streett to convert the acceptance conditions. 3047 3048 * genltl learned three new families: --dac-patterns=1..45, 3049 --eh-patterns=1..12, and --sb-patterns=1..27. Unlike other options 3050 these do not output scalable patterns, but simply a list of formulas 3051 appearing in these three papers: Dwyer et al (FMSP'98), Etessami & 3052 Holzmann (Concur'00), Somenzi & Bloem (CAV'00). 3053 3054 * genltl learned two options, --positive and --negative, to control 3055 wether formulas should be output after negation or not (or both). 3056 3057 * The formater used by --format (for ltlfilt, ltlgrind, genltl, 3058 randltl) or --stats (for autfilt, dstar2tgba, ltl2tgba, ltldo, 3059 randaut) learned to recognize double-quoted fields and double the 3060 double-quotes output inbetween as expected from RFC4180-compliant 3061 CSV files. For instance 3062 ltl2tgba -f 'a U "b+c"' --stats='"%f",%s' 3063 will output 3064 "a U ""b+c""",2 3065 3066 * The --csv-escape option of genltl, ltlfilt, ltlgrind, and randltl 3067 is now deprecated. The option is still here, but hidden and 3068 undocumented. 3069 3070 * The --stats option of autfilt, dstar2tgba, ltl2tgba, ltldo, 3071 randaut learned to display the output (or input if that makes 3072 sense) automaton as a HOA one-liner using %h (or %H), helping to 3073 create CSV files contained automata. 3074 3075 * autfilt and dstar2tgba learned to read automata from columns in 3076 CSV files, specified using the same filename/COLUMN syntax used by 3077 tools reading formulas. 3078 3079 * Arguments passed to -x (in ltl2tgba, ltl2tgta, autfilt, dstar2tgba) 3080 that are not used are now reported as they might be typos. 3081 This ocurred a couple of times in our test-suite. A similar 3082 check is done for the arguments of autfilt --sat-minimize=... 3083 3084 Library: 3085 3086 * The print_hoa() function will now output version 1.1 of the HOA 3087 format when passed the "1.1" option (i.e., use -H1.1 from any 3088 command-line tool). As far as Spot is concerned, this allows 3089 negated properties to be expressed. Version 1 of the HOA format 3090 is still the default, but we plan to default to version 1.1 in the 3091 future. 3092 3093 * The "highlight-states" and "highlight-edges" named properties, 3094 which were introduced in 1.99.8, will now be output using 3095 "spot.highlight.edges:" and "spot.highlight.states:" headers if 3096 version 1.1 of the HOA format is selected. The automaton parser 3097 was secretly able of reading that since 1.99.8, but that is now 3098 documented at https://spot.lrde.epita.fr/hoa.html#extensions 3099 3100 * highlight_nondet_states() and highlight_nondet_edges() are 3101 new functions that define the above two named properties. 3102 3103 * is_deterministic(), is_terminal(), is_weak(), and 3104 is_inherently_weak(), count_nondet_states(), 3105 highlight_nondet_edges(), highlight_nondet_states() will update 3106 the corresponding properties of the automaton as a side-effect of 3107 their check. 3108 3109 * the sbacc() function, used by "ltl2tgba -S" and "autfilt -S" to 3110 convert automata to state-based acceptance, learned some tricks 3111 (using SCCs, pulling accepting marks common to all outgoing edges, 3112 and pushing acceptance marks common to all incoming edges) to 3113 reduce the number of additional states needed. 3114 3115 * to_generalized_rabin() and to_generalized_streett() are two new 3116 functions that convert the acceptance condition as requested 3117 without changing the transition structure. 3118 3119 * language_containment_checker now has default values for all 3120 parameters of its constructor. 3121 3122 * spot::twa_run has a new method, project(), that can be used to 3123 project a run found in a product onto one of the original operand. 3124 This is for instance used by autfilt --highlight-word. 3125 3126 The old spot::project_twa_run() function has been removed: it was 3127 not used anywhere in Spot, and had an obvious bug in its 3128 implementation, so it cannot be missed by anyone. 3129 3130 * spot::twa has two new methods that supplement is_empty(): 3131 twa::accepting_run() and twa::accepting_word(). They compute 3132 what their names suggest. Note that twa::accepting_run(), unlike 3133 the two others, is currently restricted to automata with Fin-less 3134 acceptance. 3135 3136 * spot::check_stutter_invariance() can now work on non-deterministic 3137 automata for which no corresponding formula is known. This 3138 implies that "autfilt --check=stutter" will now label all 3139 automata, not just deterministic automata. 3140 3141 * New LTL and PSL simplification rules: 3142 - if e is pure eventuality and g => e, then e U g = Fg 3143 - if u is purely universal and u => g, then u R g = Gg 3144 - {s[*0..j]}[]->b = {s[*1..j]}[]->b 3145 - {s[*0..j]}<>->b = {s[*1..j]}<>->b 3146 3147 * spot::twa::succ_iterable renamed to 3148 spot::internal::twa_succ_iterable to make it clear this is not for 3149 public consumption. 3150 3151 * spot::fair_kripke::state_acceptance_conditions() renamed to 3152 spot::fair_kripke::state_acceptance_mark() for consistency. This 3153 is backward incompatible, but we are not aware of any actual use 3154 of this method. 3155 3156 Python: 3157 3158 * The __format__() method for formula supports the same 3159 operator-rewritting feature introduced in ltldo and ltlcross. 3160 So "{:[i]s}".format(f) is the same as 3161 "{:s}".format(f.unabbreviate("i")). 3162 3163 * Bindings for language_containment_checker were added. 3164 3165 * Bindings for randomize() were added. 3166 3167 * Iterating over edges via "aut.out(s)" or "aut.edges()" 3168 now allows modifying the edge fields. 3169 3170 * Under IPython the spot.ltsmin module now offers a 3171 %%pml magic to define promela models, compile them 3172 with spins, and dynamically load them. This is 3173 akin to the %%dve magic that was already supported. 3174 3175 * The %%dve and %%pml magics honor the SPOT_TMPDIR and 3176 TMPDIR environment variables. This especially helps 3177 when the current directory is read-only. 3178 3179 Documentation: 3180 3181 * A new example page shows how to test the equivalence of 3182 two LTL/PSL formulas. https://spot.lrde.epita.fr/tut04.html 3183 3184 * A new page discusses explicit vs. on-the-fly interfaces for 3185 exploring automata in C++. https://spot.lrde.epita.fr/tut50.html 3186 3187 * Another new page shows how to implement an on-the-fly Kripke 3188 structure for a custom state space. 3189 https://spot.lrde.epita.fr/tut51.html 3190 3191 * The concepts.html page now lists all named properties 3192 used by automata. 3193 3194 Bug fixes: 3195 3196 * When ltlcross found a bug using a product of complemented 3197 automata, the error message would report "Comp(Ni)*Comp(Pj)" as 3198 non-empty while the actual culprit was "Comp(Nj)*Comp(Pi)". 3199 3200 * Fix some non-deterministic execution of minimize_wdba(), causing 3201 test-suite failures with the future G++ 7, and clang 3.9. 3202 3203 * print_lbtt() had a memory leak when printing states without 3204 successors. 3205 3206New in spot 2.0.3 (2016-07-11) 3207 3208 Bug fixes: 3209 3210 * The degen-lcache=1 option of the degeneralization algorithm (which 3211 is a default option) did not behave exactly as documented: instead 3212 of reusing the first level ever created for a state where the 3213 choice of the level is free, it reused the last level ever used. 3214 This caused some posterior simulation-based reductions to be less 3215 efficient at reducing automata (on the average). 3216 * The generalized testing automata displayed by the online 3217 translator were incorrect (those output by ltl2tgta were OK). 3218 * ltl2tgta should not offer options --ba, --monitor, --tgba and such. 3219 * the relabel() function could incorrectly unregister old atomic 3220 propositions even when they were still used in the output (e.g., 3221 if a&p0 is relabeled to p0&p1). This could cause ltldo and the 3222 online translator to report errors. 3223 3224New in spot 2.0.2 (2016-06-17) 3225 3226 Documentation: 3227 3228 * We now have a citing page at https://spot.lrde.epita.fr/citing.html 3229 providing a list of references about Spot. 3230 * The Python examples have been augmented with the two examples 3231 from our ATVA'16 tool paper. 3232 3233 Bug fixes: 3234 3235 * Fix compilation error observed with Clang++ 3.7.1 and GCC 6.1.1 3236 headers. 3237 * Fix an infinite recursion in relabel_bse(). 3238 * Various small typos and cosmetic cleanups. 3239 3240New in spot 2.0.1 (2016-05-09) 3241 3242 Library: 3243 3244 * twa::unregister_ap() and twa_graph::remove_unused_ap() are new 3245 methods introduced to fix some of the bugs listed below. 3246 3247 Documentation: 3248 3249 * Add missing documentation for the option string passed to 3250 spot::make_emptiness_check_instantiator(). 3251 3252 * There is now a spot(7) man page listing all installed 3253 command-line tools. 3254 3255 Python: 3256 3257 * The tgba_determinize() function is now accessible in Python. 3258 3259 Bug fixes: 3260 3261 * The automaton parser would choke on comments like /******/. 3262 * check_strength() should also set negated properties. 3263 * Fix autfilt to apply --simplify-exclusive-ap only after 3264 the simplifications of (--small/--deterministic) have 3265 been performed. 3266 * The automaton parser did not fully register atomic propositions 3267 for automata read from never claim or as LBTT. 3268 * spot::ltsmin::kripke() had the same issue. 3269 * The sub_stats_reachable() function used to count the number 3270 of transitions based on the number of atomic propositions 3271 actually *used* by the automaton instead of using the number 3272 of AP declared. 3273 * print_hoa() will now output all the atomic propositions that have 3274 been registered, not only those that are used in the automaton. 3275 (Note that it will also throw an exception if the automaton uses 3276 an unregistered AP; this is how some of the above bugs were 3277 found.) 3278 * For Small or Deterministic preference, the postprocessor 3279 will now unregister atomic propositions that are no longer 3280 used in labels. Simplification of exclusive properties 3281 and remove_ap::strip() will do similarly. 3282 * bench/ltl2tgba/ was not working since the source code 3283 reorganization of 1.99.7. 3284 * Various typos and minor documentation fixes. 3285 3286 3287New in spot 2.0 (2016-04-11) 3288 3289 Command-line tools: 3290 3291 * ltlfilt now also support the --accept-word=WORD and 3292 --reject-word=WORD options that were introduced in autfilt in the 3293 previous version. 3294 3295 Python: 3296 3297 * The output of spot.atomic_prop_collect() is printable and 3298 can now be passed directly to spot.ltsmin.model.kripke(). 3299 3300 Library: 3301 3302 * digraph::valid_trans() renamed to digraph::is_valid_edge(). 3303 3304 Documentation: 3305 3306 * The concepts page (https://spot.lrde.epita.fr/concepts.html) now 3307 includes a highlevel description of the architecture, and some 3308 notes aboute automata properties. 3309 3310 * More Doxygen documentation for spot::formula and spot::digraph. 3311 3312New in spot 1.99.9 (2016-03-14) 3313 3314 Command-line tools: 3315 3316 * autfilt has two new options: --accept-word=WORD and 3317 --reject-word=WORD for filtering automata that accept or reject 3318 some word. The option may be used multiple times. 3319 3320 Library: 3321 3322 * The parse_word() function can be used to parse a lasso-shaped 3323 word and build a twa_word. The twa_word::as_automaton() 3324 method can be used to create an automaton out of that. 3325 * twa::ap_var() renamed to twa::ap_vars(). 3326 * emptiness_check_instantiator::min_acceptance_conditions() and 3327 emptiness_check_instantiator::max_acceptance_conditions() renamed 3328 to emptiness_check_instantiator::min_sets() and 3329 emptiness_check_instantiator::max_sets(). 3330 * tgba_reachable_iterator (and subclasses) was renamed to 3331 twa_reachable_iterator for consistency. 3332 3333 Documentation: 3334 3335 * The page https://spot.lrde.epita.fr/upgrade2.html should help 3336 people migrating old C++ code written for Spot 1.2.x, and update 3337 it for (the upcoming) Spot 2.0. 3338 3339 Bug fixes: 3340 3341 * spot/twaalgos/gtec/gtec.hh was incorrectly installed as 3342 spot/tgbaalgos/gtec/gtec.hh. 3343 * The shared libraries should now compile again on Darwin. 3344 3345New in spot 1.99.8 (2016-02-18) 3346 3347 Command-line tools: 3348 3349 * ltl2tgba now also support the --generic option (already supported 3350 by ltldo and autfilt) to lift any restriction on the acceptance 3351 condition produced. This option now has a short version: -G. 3352 3353 * ltl2tgba and autfilt have learnt how to determinize automata. 3354 For this to work, --generic acceptance should be enabled (this 3355 is the default for autfilt, but not for ltl2tgba). 3356 3357 "ltl2tgba -G -D" will now always outpout a deterministic automaton. 3358 It can be an automaton with transition-based parity acceptance in 3359 case Spot could not find a deterministic automaton with (maybe 3360 generalized) Büchi acceptance. 3361 3362 "ltl2tgba -D" is unchanged (the --tgba acceptance is the default), 3363 and will output a deterministic automaton with (generalized) Büchi 3364 acceptance only if one could be found. Otherwise a 3365 non-deterministic automaton is output, but this does NOT mean that 3366 no deterministic Büchi automaton exist for this formula. It only 3367 means Spot could not find it. 3368 3369 "autfilt -D" will determinize any automaton, because --generic 3370 acceptance is the default for autfilt. 3371 3372 "autfilt -D --tgba" will behave like "ltl2tgba -D", i.e., it may 3373 fail to find a deterministic automaton (even if one exists) and 3374 return a nondeterministic automaton. 3375 3376 * "autfilt --complement" now also works for non-deterministic 3377 automata but will output a deterministic automaton. 3378 "autfilt --complement --tgba" will likely output a 3379 nondeterministic TGBA. 3380 3381 * autfilt has a new option, --included-in, to filter automata whose 3382 language are included in the language of a given automaton. 3383 3384 * autfilt has a new option, --equivalent-to, to filter automata 3385 that are equivalent (language-wise) to a given automaton. 3386 3387 * ltlcross has a new option --determinize to instruct it to 3388 complement non-deterministic automata via determinization. This 3389 option is not enabled by default as it can potentially be slow and 3390 generate large automata. When --determinize is given, option 3391 --product=0 is implied, since the tests based on products with 3392 random state-space are pointless for deterministic automata. 3393 3394 * ltl2tgba and ltldo now support %< and %> in the string passed 3395 to --stats when reading formulas from a CSV file. 3396 3397 * ltlfilt's option --size-min=N, --size-max=N, --bsize-min=N, and 3398 --bsize-max=N have been reimplemented as --size=RANGE and 3399 --bsize=RANGE. The old names are still supported for backward 3400 compatibility, but they are not documented anymore. 3401 3402 * ltlfilt's option --ap=N can now take a RANGE as parameter. 3403 3404 * autfilt now has a --ap=RANGE option to filter automata by number 3405 of atomic propositions. 3406 3407 Library: 3408 3409 * Building products with different dictionaries now raise an 3410 exception instead of using an assertion that could be disabled. 3411 3412 * The load_ltsmin() function has been split in two. Now you should 3413 first call ltsmin_model::load(filename) to create an ltsmin_model, 3414 and then call the ltsmin_model::kripke(...) method to create an 3415 automaton that can be iterated on the fly. The intermediate 3416 object can be queried about the supported variables and their 3417 types. 3418 3419 * print_dot() now accepts several new options: 3420 - use "<N" to specify a maximum number of states to output. 3421 Incomplete states are then marked appropriately. For a quick 3422 example, compare 3423 ltl2tgba -D 'Ga | Gb | Gc' -d'<3' 3424 with 3425 ltl2tgba -D 'Ga | Gb | Gc' -d 3426 - use "C(color)" to specify the color to use for filling states. 3427 - use "#" to display the internal number of each transition 3428 - use "k" to use state-based labels when possible. This is 3429 similar to the "k" option already supported by print_hoa(), and 3430 is useful when printing Kripke structures. 3431 3432 * Option "k" is automatically used by print_dot() and print_hoa() 3433 when printing Kripke structures. 3434 3435 * print_dot() also honnor two new automaton properties called 3436 "highlight-edges" and "highlight-states". These are used to color 3437 a subset of edges or transitions. 3438 3439 * There is a new tgba_determinize() function. Despite its name, it 3440 in facts works on transition-based Büchi automaton, and will first 3441 degeneralize any automaton with generalized Büchi acceptance. 3442 3443 * The twa_safra_complement class has been removed. Use 3444 tgba_determinize() and dtwa_complement() instead. 3445 3446 * The twa::transition_annotation() and 3447 twa::compute_support_conditions() methods have been removed. 3448 3449 * The interface for all functions parsing formulas (LTL, PSL, SERE, 3450 etc.) has been changed to use an interface similar to the one used 3451 for parsing automata. These function now return a parsed_formula 3452 object that includes both a formula and a list of syntax errors. 3453 3454 Typically a function written as 3455 3456 spot::formula read(std::string input) 3457 { 3458 spot::parse_error_list pel; 3459 spot::formula f = spot::parse_infix_psl(input, pel); 3460 if (spot::format_parse_errors(std::cerr, input, pel)) 3461 exit(2); 3462 return f; 3463 } 3464 3465 should be updated to 3466 3467 spot::formula read(std::string input) 3468 { 3469 spot::parsed_formula pf = spot::parse_infix_psl(input); 3470 if (pf.format_errors(std::cerr)) 3471 exit(2); 3472 return pf.f; 3473 } 3474 3475 Python: 3476 3477 * The ltsmin interface has been binded in Python. It also 3478 comes with a %%dve cell magic to edit DiVinE models in the notebook. 3479 See https://spot.lrde.epita.fr/ipynb/ltsmin.html for a short example. 3480 3481 * spot.setup() sets de maximum number of states to display in 3482 automata to 50 by default, as more states is likely to be 3483 unreadable (and slow to process by GraphViz). This can be 3484 overridden by calling spot.setup(max_states=N). 3485 3486 * Automata now have methods to color selected states and 3487 transitions. See 3488 https://spot.lrde.epita.fr/ipynb/highlighting.html for an example. 3489 3490 Documentation: 3491 3492 * There is a new page giving informal illustrations (and extra 3493 pointers) for some concepts used in Spot. 3494 See https://spot.lrde.epita.fr/concepts.html 3495 3496 Bug fixes: 3497 3498 * Using ltl2tgba -U would fail to output the unambiguous property 3499 (regression introduced in 1.99.7) 3500 * ltlfilt, autfilt, randltl, and randaut could easily crash when 3501 compiled statically (i.e., with configure --disable-shared). 3502 * "1 U (a | Fb)" was not always simplified to "F(a | b)". 3503 * destroying the operands of an otf_product() before the product 3504 itself could crash. 3505 3506New in spot 1.99.7 (2016-01-15) 3507 3508 Command-line tools: 3509 3510 * BACKWARD INCOMPATIBLE CHANGE: All tools that output automata now 3511 use the HOA format by default instead of the GraphViz output. 3512 This makes it easier to pipe several commands together. 3513 3514 If you have an old script that relies on GraphViz being the default 3515 output and that you do not want to update it, use 3516 export SPOT_DEFAULT_FORMAT=dot 3517 to get the old behavior back. 3518 3519 * Tools that output automata now accept -d as a shorthand for --dot 3520 since requesting the GraphViz (a.k.a. dot) output by hand is now 3521 more frequent. 3522 randaut's short option for specifying edge-density used to be -d: 3523 it has been renamed to -e. 3524 3525 * The SPOT_DEFAULT_FORMAT environment variable can be set to 'dot' 3526 or 'hoa' to force a default output format for automata. Additional 3527 options may also be added, as in SPOT_DEFAULT_FORMAT='hoa=iv'. 3528 3529 * autfilt has a new option: --is-inherently-weak. 3530 3531 * The --check=strength option of all tools that produce automata 3532 will also test if an automaton is inherently weak. 3533 3534 Library: 3535 3536 * Installed headers now assume that they will be included as 3537 #include <spot/subdir/header.hh> 3538 instead of 3539 #include <subdir/header.hh> 3540 3541 This implies that when Spot headers are installed in 3542 /usr/include/spot/... (the default when using the Debian packages) 3543 or /usr/local/include/spot/... (the default when compiling from 3544 source), then it is no longuer necessary to add 3545 -I/usr/include/spot or -I/usr/local/include/spot when compiling, 3546 as /usr/include and /usr/local/include are usually searched by 3547 default. 3548 3549 Inside the source distribution, the subdirectory src/ has been 3550 renamed to spot/, so that the root of the source tree can also be 3551 put on the preprocessor's search path to compile against a 3552 non-installed version of Spot. Similarly, iface/ltsmin/ has been 3553 renamed to spot/ltsmin/, so that installed and non-installed 3554 directories can be used similarly. 3555 3556 * twa::~twa() is now calling 3557 get_dict()->unregister_all_my_variable(this); 3558 so this does not need to be done in any subclass. 3559 3560 * is_inherently_weak_automaton() is a new function, and 3561 check_strength() has been modified to also check inherently weak 3562 automata. 3563 3564 * decompose_strength() is now extracting inherently weak SCCs 3565 instead of just weak SCCs. This gets rid of some corner cases 3566 that used to require ad hoc handling. 3567 3568 * acc_cond::acc_code's methods append_or(), append_and(), and 3569 shift_left() have been replaced by operators |=, &=, <<=, and for 3570 completeness the operators |, &, and << have been added. 3571 3572 * Several methods have been removed from the acc_cond 3573 class because they were simply redundant with the methods of 3574 acc_cond::mark_t, and more complex to use. 3575 3576 acc_cond::marks(...) -> use acc_cond::mark_t(...) 3577 acc_cond::sets(m) -> use m.sets() 3578 acc_cond::has(m, u) -> use m.has(u) 3579 acc_cond::cup(l, r) -> use l | r 3580 acc_cond::cap(l, r) -> use l & r 3581 acc_cond::set_minus(l, r) -> use l - r 3582 3583 Additionally, the following methods/functions have been renamed: 3584 3585 acc_cond::is_tt() -> acc_cond::is_t() 3586 acc_cond::is_ff() -> acc_cond::is_f() 3587 parse_acc_code() -> acc_cond::acc_code(...) 3588 3589 * Automata property flags (those that tell whether the automaton is 3590 deterministic, weak, stutter-invariant, etc.) are now stored using 3591 three-valued logic: in addition to "maybe"/"yes" they can now also 3592 represent "no". This is some preparation for the upcomming 3593 support of the HOA v1.1 format, but it also saves time in some 3594 algorithms (e.g, is_deterministic() can now return immediately on 3595 automata marked as not deterministic). 3596 3597 * The automaton parser now accept negated properties as they will be 3598 introduced in HOA v1.1, and will check for some inconsistencies. 3599 These properties are stored and used when appropriate, but they 3600 are not yet output by the HOA printer. 3601 3602 Python: 3603 3604 * Iterating over the transitions leaving a state (the 3605 twa_graph::out() C++ function) is now possible in Python. See 3606 https://spot.lrde.epita.fr/tut21.html for a demonstration. 3607 3608 * Membership to acceptance sets can be specified using Python list 3609 when calling for instance the Python version of twa_graph::new_edge(). 3610 See https://spot.lrde.epita.fr/tut22.html for a demonstration. 3611 3612 * Automaton states can be named via the set_state_names() method. 3613 See https://spot.lrde.epita.fr/ipynb/product.html for an example. 3614 3615 Documentation: 3616 3617 * There is a new page explaining how to compile example programs and 3618 and link them with Spot. https://spot.lrde.epita.fr/compile.html 3619 3620 * Python bindings for manipulating acceptance conditions are 3621 demonstrated by https://spot.lrde.epita.fr/ipynb/acc_cond.html, 3622 and a Python implementation of the product of two automata is 3623 illustrated by https://spot.lrde.epita.fr/ipynb/product.html 3624 3625 Source code reorganisation: 3626 3627 * A lot of directories have been shuffled around in the 3628 distribution: 3629 src/ -> spot/ (see rational above) 3630 iface/ltsmin/ (code) -> spot/ltsmin/ 3631 wrap/python/ -> python/ 3632 src/tests/ -> tests/core/ 3633 src/sanity/ -> tests/sanity/ 3634 iface/ltsmin/ (tests) -> tests/ltsmin/ 3635 wrap/python/tests -> tests/python/ 3636 3637 Bug fixes: 3638 3639 * twa_graph would incorrectly replace named-states during 3640 purge_dead_states and purge_unreachable_states. 3641 * twa::ap() would contain duplicates when an atomic proposition 3642 was registered several times. 3643 * product() would incorrectly mark the product of two 3644 sttuter-sensitive automata as stutter-sensitive as well. 3645 * complete() could incorrectly reuse an existing (but accepting!) 3646 state as a sink. 3647 3648New in spot 1.99.6 (2015-12-04) 3649 3650 Command-line tools: 3651 3652 * autfilt has two new filters: --is-weak and --is-terminal. 3653 3654 * autfilt has a new transformation: --decompose-strength, 3655 implementing the decomposition of our TACAS'13 paper. 3656 A demonstration of this feature via the Python bindings 3657 can be found at https://spot.lrde.epita.fr/ipynb/decompose.html 3658 3659 * All tools that output HOA files accept a --check=strength option 3660 to request automata to be marked as "weak" or "terminal" as 3661 appropriate. Without this option, these properties may only be 3662 set as a side-effect of running transformations that use this 3663 information. 3664 3665 Library: 3666 3667 * Properties of automata (like the "properties:" line of the HOA 3668 format) are stored as bits whose interpretation is True=yes, 3669 False=maybe. Having getters like "aut->is_deterministic()" or 3670 "aut->is_unambiguous()" was confusing, because there are separate 3671 functions "is_deterministic(aut)" and "is_unambiguous(aut)" that 3672 do actually check the automaton. The getters have been renamed to 3673 avoid confusion, and get names more in line with the HOA format. 3674 3675 - twa::has_state_based_acc() -> twa::prop_state_acc() 3676 - twa::prop_state_based_acc(bool) -> twa::prop_state_acc(bool) 3677 - twa::is_inherently_weak() -> twa::prop_inherently_weak() 3678 - twa::is_deterministic() -> twa::prop_deterministic() 3679 - twa::is_unambiguous() -> twa::prop_unambiguous() 3680 - twa::is_stutter_invariant() -> twa::prop_stutter_invariant() 3681 - twa::is_stutter_sensitive() -> twa::prop_stutter_sensitive() 3682 3683 The setters have the same names as the getters, except they take a 3684 Boolean argument. This argument used to be optionnal (defaulting 3685 to True), but it no longer is. 3686 3687 * Automata now support the "weak" and "terminal" properties in 3688 addition to the previously supported "inherently-weak". 3689 3690 * By default the HOA printer tries not to bloat the output with 3691 properties that are redundant and probably useless. The HOA 3692 printer now has a new option "v" (use "-Hv" from the command line) 3693 to output more verbose "properties:". This currently includes 3694 outputing "no-univ-branch", outputting "unambiguous" even for 3695 automata already tagged as "deterministic", and "inherently-weak" 3696 or "weak" even for automata tagged "weak" or "terminal". 3697 3698 * The HOA printer has a new option "k" (use "-Hk" from the command 3699 line) to output automata using state labels whenever possible. 3700 This is useful to print Kripke structures. 3701 3702 * The dot output will display pair of states when displaying an 3703 automaton built as an explicit product. This works in IPython 3704 with spot.product() or spot.product_or() and in the shell with 3705 autfilt's --product or --product-or options. 3706 3707 * The print_dot() function supports a new option, +N, where N is a 3708 positive integer that will be added to all set numbers in the 3709 output. This is convenient when displaying two automata before 3710 building their product: use +N to shift the displayed sets of the 3711 second automaton by the number of acceptance sets N of the first 3712 one. 3713 3714 * The sat minimization for DTωA now does a better job at selecting 3715 reference automata when the output acceptance is the the same as 3716 the input acceptance. This can provide nice speedups when tring 3717 to syntethise larged automata with different acceptance 3718 conditions. 3719 3720 * Explicit Kripke structures (i.e., stored as explicit graphs) have 3721 been rewritten above the graph class, using an interface similar 3722 to the twa class. The new class is called kripke_graph. The ad 3723 hoc Kripke parser and printer have been removed, because we can 3724 now use print_hoa() with the "k" option to print Kripke structure 3725 in the HOA format, and furthermore the parse_aut() function now 3726 has an option to load such an HOA file as a kripke_graph. 3727 3728 * The HOA parser now accepts identifier, aliases, and headernames 3729 containing dots, as this will be allowed in the next version of 3730 the HOA format. 3731 3732 * Renamings: 3733 is_guarantee_automaton() -> is_terminal_automaton() 3734 tgba_run -> twa_run 3735 twa_word::print -> operator<< 3736 dtgba_sat_synthetize() -> dtwa_sat_synthetize() 3737 dtgba_sat_synthetize_dichotomy() -> dtwa_sat_synthetize_dichotomy() 3738 3739 Python: 3740 3741 * Add bindings for is_unambiguous(). 3742 * Better interface for sat_minimize(). 3743 3744 Bug fixes: 3745 3746 * the HOA parser was ignoring the "unambiguous" property. 3747 * --dot=Bb should work like --dot=b, allowing us to disable 3748 a B option set via an environment variable. 3749 3750New in spot 1.99.5 (2015-11-03) 3751 3752 Command-line tools: 3753 3754 * autfilt has gained a --complement option. 3755 It currently works only for deterministic automata. 3756 3757 * By default, autfilt does not simplify automata (this has not 3758 changed), as if the --low --any options were used. But now, if 3759 one of --small, --deterministic, or --any is given, the 3760 optimization level automatically defaults to --high (unless 3761 specified otherwise). For symmetry, if one of --low, --medium, or 3762 --high is given, then the translation intent defaults to --small 3763 (unless specified otherwise). 3764 3765 * autfilt, dstar2tgba, ltlcross, and ltldo now trust the (supported) 3766 automaton properties declared in any HOA file they read. This can 3767 be disabled with option --trust-hoa=no. 3768 3769 * ltlgrind FILENAME[/COL] is now the same as 3770 ltlgrind -F FILENAME[/COL] for consistency with ltlfilt. 3771 3772 Library: 3773 3774 * dtgba_complement() was renamed to dtwa_complement(), moved to 3775 complement.hh, and its purpose was restricted to just completing 3776 the automaton and complementing its acceptance condition. Any 3777 further acceptance condition transformation can be done with 3778 to_generalized_buchi() or remove_fin(). 3779 3780 * The remove_fin() has learnt how to better deal with automata that 3781 are declared as weak. This code was previously in 3782 dtgba_complement(). 3783 3784 * scc_filter_states() has learnt to remove useless acceptance marks 3785 that are on transitions between SCCs, while preserving state-based 3786 acceptance. The most visible effect is in the output of "ltl2tgba 3787 -s XXXa": it used to have 5 accepting states, it now has only one. 3788 (Changing removing acceptance of those 4 states has no effect on 3789 the language, but it speeds up some algorithms like NDFS-based 3790 emptiness checks, as discussed in our Spin'15 paper.) 3791 3792 * The HOA parser will diagnose any version that is not v1, unless it 3793 looks like a subversion of v1 and no parse error was detected. 3794 3795 * The way to pass option to the automaton parser has been changed to 3796 make it easier to introduce new options. One such new option is 3797 "trust_hoa": when true (the default) supported properties declared 3798 in HOA files are trusted even if they cannot be easily be verified. 3799 Another option "raise_errors" now replaces the method 3800 automaton_stream_parser::parse_strict(). 3801 3802 * The output of the automaton parser now include the list of parse 3803 errors (that does not have to be passed as a parameters) and the 3804 input filename (making the output of error messages easier). 3805 3806 * The following renamings make the code more consistent: 3807 ltl_simplifier -> tl_simplifier 3808 tgba_statistics::transitions -> twa_statistics::edges 3809 tgba_sub_statistics::sub_transitions -> twa_sub_statistics::transitions 3810 tgba_run -> twa_run 3811 reduce_run -> twa_run::reduce 3812 replay_tgba_run -> twa_run::replay 3813 print_tgba_run -> operator<< 3814 tgba_run_to_tgba -> twa_run::as_twa 3815 format_parse_aut_errors -> parsed_aut::format_errors 3816 twa_succ_iterator::current_state -> twa_succ_iterator::dst 3817 twa_succ_iterator::current_condition -> twa_succ_iterator::cond 3818 twa_succ_iterator::current_acceptance_conditions -> twa_succ_iterator::acc 3819 ta_succ_iterator::current_state -> ta_succ_iterator::dst 3820 ta_succ_iterator::current_condition -> ta_succ_iterator::cond 3821 ta_succ_iterator::current_acceptance_conditions -> ta_succ_iterator::acc 3822 3823 Python: 3824 3825 * The minimum supported Python version is now 3.3. 3826 * Add bindings for complete() and dtwa_complement() 3827 * Formulas now have a custom __format__ function. See 3828 https://spot.lrde.epita.fr/tut01.html for examples. 3829 * The Debian package is now compiled for all Python3 versions 3830 supported by Debian, not just the default one. 3831 * Automata now have get_name()/set_name() methods. 3832 * spot.postprocess(aut, *options), or aut.postprocess(*options) 3833 simplify the use of the spot.postprocessor object. (Just like we 3834 have spot.translate() on top of spot.translator().) 3835 * spot.automata() and spot.automaton() now have additional 3836 optional arguments: 3837 - timeout: to restrict the runtime of commands that 3838 produce automata 3839 - trust_hoa: can be set to False to ignore HOA properties 3840 that cannot be easily verified 3841 - ignore_abort: can be set to False if you do not want to 3842 skip automata ended with --ABORT--. 3843 3844 Documentation: 3845 3846 * There is a new page showing how to use spot::postprocessor 3847 to convert any type of automaton to Büchi. 3848 https://spot.lrde.epita.fr/tut30.html 3849 3850 Bugs fixed: 3851 3852 * Work around some weird exception raised when using the 3853 randltlgenerator under Python 3.5. 3854 * Recognize "nullptr" formulas as None in Python. 3855 * Fix compilation of bench/stutter/ 3856 * Handle saturation of formula reference counts. 3857 * Fix typo in the Python code for the CGI server. 3858 * "randaut -Q0 1" used to segfault. 3859 * "ltlgrind -F FILENAME/COL" did not preserve other CSV columns. 3860 * "ltlgrind --help" did not document FORMAT. 3861 * unabbreviate could easily use forbidden operators. 3862 * "autfilt --is-unambiguous" could fail to detect the nonambiguity 3863 of some automata with empty languages. 3864 * When parsing long tokens (e.g, state labels representing 3865 very large strings) the automaton parser could die with 3866 "input buffer overflow, can't enlarge buffer because scanner uses REJECT" 3867 3868New in spot 1.99.4 (2015-10-01) 3869 3870 New features: 3871 3872 * autfilt's --sat-minimize now takes a "colored" option to constrain 3873 all transitions (or states) in the output automaton to belong to 3874 exactly one acceptance sets. This is useful when targeting parity 3875 acceptance. 3876 3877 * autfilt has a new --product-or option. This builds a synchronized 3878 product of two (completed of needed) automata in order to 3879 recognize the *sum* of their languages. This works by just using 3880 the disjunction of their acceptance conditions (with appropriate 3881 renumbering of the acceptance sets). 3882 3883 For consistency, the --product option (that builds a synchronized 3884 product that recognizes the *intersection* of the languages) now 3885 also has a --product-and alias. 3886 3887 * the parser for ltl2dstar's format has been merged with the parser 3888 for the other automata formats. This implies two things: 3889 - autfilt and dstar2tgba (despite its name) can now both read 3890 automata written in any of the four supported syntaxes 3891 (ltl2dstar's, lbtt's, HOA, never claim). 3892 - "dstar2tgba some files..." now behaves exactly like 3893 "autfilt --tgba --high --small some files...". 3894 (But dstar2tgba does not offer all the filtering and 3895 transformations options of autfilt.) 3896 3897 Major code changes and reorganization: 3898 3899 * The class hierarchy for temporal formulas has been entirely 3900 rewritten. This change is actually quite massive (~13200 lines 3901 removed, ~8200 lines added), and brings some nice benefits: 3902 - LTL/PSL formulas are now represented by lightweight formula 3903 objects (instead of pointers to children of an abstract 3904 formula class) that perform reference counting automatically. 3905 - There is no hierachy anymore: all operators are represented by 3906 a single type of node in the syntax tree, and an enumerator is 3907 used to distinguish between operators. 3908 - Visitors have been replaced by member functions such as map() 3909 or traverse(), that take a function (usually written as a 3910 lambda function) and apply it to the nodes of the tree. 3911 - As a consequence, writing algorithms that manipulate formula 3912 is more friendly, and several algorithms that spanned a few 3913 pages have been reduced to a few lines. 3914 The page https://spot.lrde.epita.fr/tut03.html illustrates the 3915 new interface, in both C++ and Python. 3916 3917 * Directories ltlast/, ltlenv/, and ltlvisit/, have been merged into 3918 a single tl/ directory (for temporal logic). This is motivated by 3919 the fact that these formulas are not restricted to LTL, and by the 3920 fact that we no longuer use the "visitor" pattern. 3921 3922 * The LTL/PSL parser is now declared in tl/parse.hh (instead of 3923 ltlparse/public.hh). 3924 3925 * The spot::ltl namespace has been merged with the spot namespace. 3926 3927 * The dupexp_dfs() function has been renamed to copy(), and has 3928 learned to preserve named states if required. 3929 3930 * Atomic propositions can be declared without going through an 3931 environment using the spot::formula::ap() static function. They 3932 can be registered for an automaton directly using the 3933 spot::twa::register_ap() method. The vector of atomic 3934 propositions used by an automaton can now be retrieved using the 3935 spot::twa::ap() method. 3936 3937New in spot 1.99.3 (2015-08-26) 3938 3939 * The CGI script for LTL translation offers a HOA download link 3940 for each generated automaton. 3941 3942 * The html documentation now includes a HTML copies of the man 3943 pages, and HTML copies of the Python notebooks. 3944 3945 * scc_filter(aut, true) does not remove Fin marks from rejecting 3946 SCCs, but it now does remove Fin marks from transitions between 3947 SCCs. 3948 3949 * All the unabbreviation functions (unabbreviate_ltl(), 3950 unabbreviate_logic(), unabbreviate_wm()) have been merged into a 3951 single unabbreviate() function that takes a string representing 3952 the list of operators to remove among "eFGiMRW^" where 'e', 'i', 3953 and '^' stand respectively for <->, ->, and xor. 3954 This feature is also available via ltlfilt --unabbreviate. 3955 3956 * In LTL formulas, atomic propositions specified using double-quotes 3957 can now include \" and \\. (This is more consistent with the HOA 3958 format, which already allows that.) 3959 3960 * All the conversion routines that were written specifically for 3961 ltl2dstar's output format (DRA->BA & DRA->TGBA) have been ported 3962 to the new TωA structure supporting the HOA format. The DRA->TGBA 3963 conversion was reimplemented in the previous release, and the 3964 DRA->BA conversion has been reimplemented in this release (but it 3965 is still restricted to state-based acceptance). All these 3966 conversions are called automatically by to_generalized_buchi() 3967 or remove_fin() so there should be no need to call them directly. 3968 3969 As a consequence: 3970 - "autfilt --remove-fin" or "autfilt -B" is better at converting 3971 state-based Rabin automata: it will produce a DBA if the input is 3972 deterministic and DBA-realizable, but will preserve as much 3973 determinism as possible otherwise. 3974 - a lot of obsolete code that was here only to support the old 3975 conversion routines has been removed. (The number of lines 3976 removed by this release is twice the number of lines added.) 3977 - ltlcross now uses automata in ltl2dstar's format directly, 3978 without converting them to Büchi (this makes the statistics 3979 reported in CSV files more relevant). 3980 - ltlcross no longer outputs additional columns about the size 3981 of the input automaton in the case ltl2dstar's format is used. 3982 - ltldo uses results in ltl2dstar's format directly, without 3983 converting them to Büchi. 3984 - dstar2tgba has been greatly simplified and now uses the 3985 same output routines as all the other tools that output 3986 automata. This implies a few minor semantic changes, for 3987 instance --stats=%A used to output the number of acceptance 3988 *pairs* in the input automaton, while it now outputs the 3989 number of acceptance sets like in all the other tools. 3990 3991 * Bugs fixed 3992 - Some acceptance conditions like Fin(0)|Fin(1)|Fin(2)&Inf(3) 3993 were not detected as generalized-Rabin. 3994 - Unknown arguments for print_hoa() (i.e., option -H in command-line 3995 tools) are now diagnosed. 3996 - The CGI script for LTL translation now forces transition-based 3997 acceptance on WDBA-minimized automata when TGBA is requested. 3998 - ltlgrind --help output had some options documented twice, or 3999 in the wrong place. 4000 - The man page for ltlcross had obsolete examples. 4001 - When outputting atomic propositions in double quotes, the 4002 escaping routine used by the two styles of LaTeX output was 4003 slightly wrong. For instance ^ was incorrectly escaped, and 4004 the double quotes where not always properly rendered. 4005 - A spurious assertion was triggered by streett_to_generalized_buchi(), 4006 but only when compiled in DEBUG mode. 4007 - LTL formula rewritten in Spin's syntax no longer have their -> 4008 and <-> rewritten away. 4009 - Fix some warnings reported by the development version of GCC 6. 4010 - The spot.translate() function of the Python binding had a typo 4011 preventing the use of 'low'/'medium'/'high' as argument. 4012 - Fix spurious failure of uniq.test under different locales. 4013 - ltlcross now recovers from out-of-memory errors during 4014 state-space products. 4015 - bitvect.test was failing on 32bit architectures with 4016 assertions enabled because of a bug in the test case. 4017 4018New in spot 1.99.2 (2015-07-18) 4019 4020 * The scc_info object, used to build a map of SCCs while gathering 4021 additional information, has been simplified and speed up. One 4022 test case where ltlcross would take more than 13min (to check the 4023 translation of one PSL formula) now takes only 75s. 4024 4025 * streett_to_generalized_buchi() is a new function that implements 4026 what its name suggests, with some SCC-based optimizations over the 4027 naive definition. It is used by the to_generalized_buchi() and 4028 remove_fin() functions when the input automaton is a Streett 4029 automaton with more than 3 pairs (this threeshold can be changed 4030 via the SPOT_STREETT_CONV_MIN environment variable -- see the 4031 spot-x(7) man page for details). 4032 4033 This is mainly useful to ltlcross, which has to get rid of "Fin" 4034 acceptance to perform its checks. As an example, the Streett 4035 automaton generatated by ltl2dstar (configured with ltl2tgba) for 4036 the formula 4037 !((GFa -> GFb) & (GFc -> GFd)) 4038 has 4307 states and 14 acceptance sets. The new algorithm can 4039 translate it into a TGBA with 9754 states and 7 acceptance sets, 4040 while the default approch used for converting any acceptance 4041 to TGBA would produce 250967 states and 7 acceptance sets. 4042 4043 * Bugs fixed: 4044 - p[+][:*2] was not detected as belonging to siPSL. 4045 - scc_filter() would incorrectly remove Fin marks from 4046 rejecting SCCs. 4047 - the libspotltsmin library is installed. 4048 - ltlcross and ltldo did not properly quote atomic propositions 4049 and temporary file names containing a single-quote. 4050 - a missing Python.h is now diagnosed at ./configure time, with 4051 the suggestion to either install python3-devel, or run 4052 ./configure --disable-python. 4053 - Debian packages for libraries have been split from 4054 the main Spot package, as per Debian guidelines. 4055 4056New in spot 1.99.1 (2015-06-23) 4057 4058 * Major changes motivating the jump in version number 4059 4060 - Spot now works with automata that can represent more than 4061 generalized Büchi acceptance. Older versions were built around 4062 the concept of TGBA (Transition-based Generalized Büchi 4063 Automata) while this version now deals with what we call TωA 4064 (Transition-based ω-Automata). TωA support arbitrary acceptance 4065 conditions specified as a Boolean formula of transition sets 4066 that must be visited infinitely often or finitely often. This 4067 genericity allows for instance to represent Rabin or Streett 4068 automata, as well as some generalized variants of those. 4069 4070 - Spot has near complete support for the Hanoi Omega Automata 4071 format. http://adl.github.io/hoaf/ This formats supports 4072 automata with the generic acceptance condition described above, 4073 and has been implemented in a number of third-party tools (see 4074 http://adl.github.io/hoaf/support.html) to ease their 4075 interactions. The only part of the format not yet implemented in 4076 Spot is the support for alternating automata. 4077 4078 - Spot is now compiling in C++11 mode. The set of C++11 features 4079 we use requires GCC >= 4.8 or Clang >= 3.5. Although GCC 4.8 is 4080 more than 2-year old, people with older installations won't be 4081 able to install this version of Spot. 4082 4083 - As a consequence of the switches to C++11 and to TωA, a lot of 4084 the existing C++ interfaces have been renamed, and sometime 4085 reworked. This makes this version of Spot not backward 4086 compatible with Spot 1.2.x. See below for the most important 4087 API changes. Furtheremore, the reason this release is not 4088 called Spot 2.0 is that we have more of those changes planned. 4089 4090 - Support for Python 2 was dropped. We now support only Python 4091 3.2 or later. The Python bindings have been improved a lot, and 4092 include some conveniance functions for better integration with 4093 IPython's rich display system. User familiar with IPython's 4094 notebook should have a look at the notebook files in 4095 wrap/python/tests/*.ipynb 4096 4097 * Major news for the command-line tools 4098 4099 - The set of tools installed by spot now consists in the following 4100 11 commands. Those marked with a '+' are new in this release. 4101 4102 - randltl Generate random LTL/PSL formulas. 4103 - ltlfilt Filter and convert LTL/PSL formulas. 4104 - genltl Generate LTL formulas from scalable patterns. 4105 - ltl2tgba Translate LTL/PSL formulas into Büchi automata. 4106 - ltl2tgta Translate LTL/PSL formulas into Testing automata. 4107 - ltlcross Cross-compare LTL/PSL-to-Büchi translators. 4108 + ltlgrind Mutate LTL/PSL formula. 4109 - dstar2tgba Convert deterministic Rabin or Streett automata into Büchi. 4110 + randaut Generate random automata. 4111 + autfilt Filter and convert automata. 4112 + ltldo Run LTL/PSL formulas through other tools. 4113 4114 randaut does not need any presentation: it does what you expect. 4115 4116 ltlgrind is a new tool that mutates LTL or PSL formulas. If you 4117 have a tool that is bogus on some formula that is too large to 4118 debug, you can use ltlgrind to generate smaller derived formulas 4119 and see if you can reproduce the bug on those. 4120 4121 autfilt is a new tool that processes a stream of automata. It 4122 allows format conversion, filtering automata based on some 4123 properties, and general transformations (e.g., change of 4124 acceptance conditions, removal of useless states, product 4125 between automata, etc.). 4126 4127 ltldo is a new tool that runs LTL/PSL formulas through other 4128 tools, but uses Spot's command-line interfaces for specifying 4129 input and output. This makes it easier to use third-party tool 4130 in a pipe, and it also takes care of some necessary format 4131 conversion. 4132 4133 - ltl2tgba has a new option, -U, to produce unambiguous automata. 4134 In unambiguous automata any word is recognized by at most one 4135 accepting run, but there might be several ways to reject a word. 4136 This works for LTL and PSL formulas. 4137 4138 - ltl2tgba has a new option, -S, to produce generalized-Büchi 4139 automata with state-based acceptance. Those are obtained by 4140 converting some transition-based GBA into a state-based GBA, so 4141 they are usually not as small as one would wish. The same 4142 option -S is also supported by autfilt. 4143 4144 - ltlcross will work with translator producing automata with any 4145 acceptance condition, provided the output is in the HOA format. 4146 So it can effectively be used to validate tools producing Rabin 4147 or Streett automata. 4148 4149 - ltlcross has several new options: 4150 4151 --grind attempts to reduce the size of any bogus formula it 4152 discovers, while still exhibiting the bug. 4153 4154 --ignore-execution-failures ignores cases where a translator 4155 exits with a non-zero status. 4156 4157 --automata save the produced automata into the CSV or JSON 4158 file. Those automata are saved using the HOA format. 4159 4160 ltlcross will also output two extra columns in its CSV/JSON 4161 output: "ambiguous_aut" and "complete_aut" are Boolean 4162 that respectively tells whether the automaton is 4163 ambiguous and complete. 4164 4165 - "ltlfilt --stutter-invariant" will now work with PSL formulas. 4166 The implementation is actually much more efficient 4167 than our previous implementation that was only for LTL. 4168 4169 - ltlfilt's old -q/--quiet option has been renamed to 4170 --ignore-errors. The new -q/--quiet semantic is the 4171 same as in grep (and also autfilt): disable all normal 4172 input, for situtations where only the exit status matters. 4173 4174 - ltlfilt's old -n/--negate option can only be used as --negate 4175 now. The short '-n NUM' option is now the same as the new 4176 --max-count=N option, for consistency with other tools. 4177 4178 - ltlfilt has a new --count option to count the number of matching 4179 automata. 4180 4181 - ltlfilt has a new --exclusive-ap option to constrain formulas 4182 based on a list of mutually exclusive atomic propositions. 4183 4184 - ltlfilt has a new option --define to be used in conjunction with 4185 --relabel or --relabel-bool to print the mapping between old and 4186 new labels. 4187 4188 - all tools that produce formulas or automata now have an --output 4189 (a.k.a. -o) option to redirect that output to a file instead of 4190 standard output. The name of this file can be constructed using 4191 the same %-escape sequences that are available for --stats or 4192 --format. 4193 4194 - all tools that output formulas have a -0 option to separate 4195 formulas with \0. This helps in conjunction with xargs -0. 4196 4197 - all tools that output automata have a --check option that 4198 request extra checks to be performed on the output to fill 4199 in properties values for the HOA format. This options 4200 implies -H for HOA output. For instance 4201 ltl2tgba -H 'formula' 4202 will declare the output automaton as 'stutter-invariant' 4203 only if the formula is syntactically stutter-invariant 4204 (e.g., in LTL\X). With 4205 ltl2tgba --check 'formula' 4206 additional checks will be performed, and the automaton 4207 will be accurately marked as either 'stutter-invariant' 4208 or 'stutter-sensitive'. Another check performed by 4209 --check is testing whether the automaton is unambiguous. 4210 4211 - ltlcross (and ltldo) have a list of hard-coded shorthands 4212 for some existing tools. So for instance running 4213 'ltlcross spin ...' is the same as running 4214 'ltlcross "spin -f %s>%N" ...'. This feature is much 4215 more useful for ltldo. 4216 4217 - For options that take an output filename (i.e., ltlcross's 4218 --save-bogus, --grind, --csv, --json) you can force the file 4219 to be opened in append mode (instead of being truncated) by 4220 by prefixing the filename with ">>". For instance 4221 --save-bogus=">>bugs.ltl" 4222 will append to the end of the file. 4223 4224 * Other noteworthy news 4225 4226 - The web site moved to http://spot.lrde.epita.fr/. 4227 4228 - We now have Debian packages. 4229 See http://spot.lrde.epita.fr/install.html 4230 4231 - The documentation now includes some simple code examples 4232 for both Python and C++. (This is still a work in progress.) 4233 4234 - The curstomized version of BuDDy (libbdd) used by Spot has be 4235 renamed as (libbddx) to avoid issues with copies of BuDDy 4236 already installed on the system. 4237 4238 - There is a parser for the HOA format 4239 (http://adl.github.io/hoaf/) available as a 4240 spot::automaton_stream_parser object or spot::parse_aut() 4241 function. The former version is able to parse a stream of 4242 automata in order to do batch processing. This format can be 4243 output by all tools (since Spot 1.2.5) using the --hoa option, 4244 and it can be read by autfilt (by default) and ltlcross (using 4245 the %H specifier). The current implementation does not support 4246 alternation. Multiple initial states are converted into an 4247 extra initial state; complemented acceptance sets Inf(!x) are 4248 converted to Inf(x); explicit or implicit labels can be used; 4249 aliases are supported; "--ABORT--" can be used in a stream. 4250 4251 - The above HOA parser can also parse never claims, and LBTT 4252 automata, so the never claim parser and the LBTT parser have 4253 been removed. This implies that autfilt can input a mix of HOA, 4254 never claims, and LBTT automata. ltlcross also use the same 4255 parser for all these output, and the old %T and %N specifiers 4256 have been deprecated and replaced by %O (for output). 4257 4258 - While not all algorithms in the library are able to work with 4259 any acceptance condition supported by the HOA format, the 4260 following two new functions mitigate that: 4261 4262 - remove_fin() takes a TωA whose accepting condition uses Fin(x) 4263 primitive, and produces an equivalent TωA without Fin(x): 4264 i.e., the output acceptance is a disjunction of generalized 4265 Büchi acceptance. This type of acceptance is supported by 4266 SCC-based emptiness-check, for instance. 4267 4268 - similarly, to_tgba() converts any TωA into an automaton with 4269 generalized-Büchi acceptance. 4270 4271 - randomize() is a new algorithm that randomly reorders the states 4272 and transitions of an automaton. It can be used from the 4273 command-line using "autfilt --randomize". 4274 4275 - the interface in iface/dve2 has been renamed to iface/ltsmin 4276 because it can now interface the dynamic libraries created 4277 either by Divine (as patched by the LTSmin group) or by 4278 Spins (the LTSmin compiler for Promela). 4279 4280 - LTL/PSL formulas can include /* comments */. 4281 4282 - PSL SEREs support a new operator [:*i..j], the iterated fusion. 4283 [:*i..j] is to the fusion operator ':' what [*i..j] is to the 4284 concatenation operator ';'. For instance (a*;b)[:*3] is the 4285 same as (a*;b):(a*;b):(a*;b). The operator [:+], is syntactic 4286 sugar for [:*1..], and corresponds to the operator ⊕ introduced 4287 by Dax et al. (ATVA'09). 4288 4289 - GraphViz output now uses an horizontal layout by default, and 4290 also use circular states (unless the automaton has more than 100 4291 states, or uses named-states). The --dot option of the various 4292 command-line tools takes an optional parameter to fine-tune the 4293 GraphViz output (including vertical layout, forced circular or 4294 elliptic states, named automata, SCC information, ordered 4295 transitions, and different ways to colorize the acceptance 4296 sets). The environment variables SPOT_DOTDEFAULT and 4297 SPOT_DOTEXTRA can also be used to respectively provide a default 4298 argument to --dot, and add extra attributes to the output graph. 4299 4300 - Never claims can now be output in the style used by Spin since 4301 version 6.2.4 (i.e., using do..od instead of if..fi, and with 4302 atomic statements for terminal acceptance). The default output 4303 is still the old one for compatibility with existing tools. The 4304 new style can be requested from command-line tools using option 4305 --spin=6 (or -s6 for short). 4306 4307 - Support for building unambiguous automata. ltl_to_tgba() has a 4308 new options to produce unambiguous TGBA (used by ltl2tgba -U as 4309 discussed above). The function is_unambiguous() will check 4310 whether an automaton is unambigous, and this is used by 4311 autfilt --is-unmabiguous. 4312 4313 - The SAT-based minimization algorithm for deterministic automata 4314 has been updated to work with ω-Automaton with any acceptance. 4315 The input and the output acceptance can be different, so for 4316 instance it is possible to create a minimal deterministic 4317 Streett automaton starting from a deterministic Rabin automaton. 4318 This functionnality is available via autfilt's --sat-minimize 4319 option. See doc/userdoc/satmin.html for details. 4320 4321 - The on-line interface at http://spot.lrde.epita.fr/trans.html 4322 can be used to check stutter-invariance of any LTL/PSL formula. 4323 4324 - The on-line interface will work around atomic propositions not 4325 supported by ltl3ba. (E.g. you can now translate F(A) or 4326 G("foo < bar").) 4327 4328 * Noteworthy code changes 4329 4330 - Boost is not used anymore. 4331 4332 - Automata are now manipulated exclusively via shared pointers. 4333 4334 - Most of what was called tgba_something is now called 4335 twa_something, unless it is really meant to work only for TGBA. 4336 This includes functions, classes, file, and directory names. 4337 For instance the class tgba originally defined in tgba/tgba.hh, 4338 has been replaced by the class twa defined in twa/twa.hh. 4339 4340 - the tgba_explicit class has been completely replaced by a more 4341 efficient twa_graph class. Many of the algorithms that were 4342 written against the abstract tgba (now twa) interface have been 4343 rewritten using twa_graph instances as input and output, making 4344 the code a lot simpler. 4345 4346 - The tgba_succ_iterator (now twa_succ_iterator) interface has 4347 changed. Methods next(), and first() should now return a bool 4348 indicating whether the current iteration is valid. 4349 4350 - The twa base class has a new method, release_iter(), that can 4351 be called to give a used iterator back to its automaton. This 4352 iterator is then stored in a protected member, iter_cache_, and 4353 all implementations of succ_iter() can be updated to recycle 4354 iter_cache_ (if available) instead of allocating a new iterator. 4355 4356 - The tgba (now called twa) base class has a new method, succ(), 4357 to support C++11' range-based for loop, and hide all the above 4358 change. 4359 4360 Instead of the following syntax: 4361 4362 tgba_succ_iterator* i = aut->succ_iter(s); 4363 for (i->first(); !i->done(); i->next()) 4364 { 4365 // use i->current_state() 4366 // i->current_condition() 4367 // i->current_acceptance_conditions() 4368 } 4369 delete i; 4370 4371 We now prefer: 4372 4373 for (auto i: aut->succ(s)) 4374 { 4375 // use i->current_state() 4376 // i->current_condition() 4377 // i->current_acceptance_conditions() 4378 } 4379 4380 And the above syntax is really just syntactic suggar for 4381 4382 twa_succ_iterator* i = aut->succ_iter(s); 4383 if (i->first()) 4384 do 4385 { 4386 // use i->current_state() 4387 // i->current_condition() 4388 // i->current_acceptance_conditions() 4389 } 4390 while (i->next()); 4391 aut->release_iter(i); // allow the automaton to recycle the iterator 4392 4393 Where the virtual calls to done() and delete have been avoided. 4394 4395 - twa::succ_iter() now takes only one argument. The optional 4396 global_state and global_automaton arguments have been removed. 4397 4398 - The following methods have been removed from the TGBA interface and 4399 all their subclasses: 4400 - tgba::support_variables() 4401 - tgba::compute_support_variables() 4402 - tgba::all_acceptance_conditions() // use acc().accepting(...) 4403 - tgba::neg_acceptance_conditions() 4404 - tgba::number_of_acceptance_conditions() // use acc().num_sets() 4405 4406 - Membership to acceptance sets are now stored using bit sets, 4407 currently limited to 32 bits. Each TωA has a acc() method that 4408 returns a reference to an acceptance object (of type 4409 spot::acc_cond), able to operate on acceptance marks 4410 (spot::acc_cond::mark_t). 4411 4412 Instead of writing code like 4413 i->current_acceptance_conditions() == aut->all_acceptance_conditions() 4414 we now write 4415 aut->acc().accepting(i->current_acceptance_conditions()) 4416 (Note that for accepting(x) to return something meaningful, x 4417 should be a set of acceptance sets visitied infinitely often. So let's 4418 imagine that in the above example i is looking at a self-loop.) 4419 4420 Similarly, 4421 aut->number_of_acceptance_conditions() 4422 is now 4423 aut->acc().num_sets() 4424 4425 - All functions used for printing LTL/PSL formulas or automata 4426 have been renamed to print_something(). Likewise the various 4427 parsers should be called parse_something() (they haven't yet 4428 all been renamed). 4429 4430 - All test suites under src/ have been merged into a single one in 4431 src/tests/. The testing tool that was called 4432 src/tgbatest/ltl2tgba has been renamed as src/tests/ikwiad 4433 (short for "I Know What I Am Doing") so that users should be 4434 less tempted to use it instead of src/bin/ltl2tgba. 4435 4436 * Removed features 4437 4438 - The long unused interface to GreatSPN (or rather, interface to 4439 a non-public, customized version of GreatSPN) has been removed. 4440 As a consequence, we could get rid of many cruft in the 4441 implementation of Couvreur's FM'99 emptiness check. 4442 4443 - Support for symbolic, BDD-encoded TGBAs has been removed. This 4444 includes the tgba_bdd_concrete class and associated supporting 4445 classes, as well as the ltl_to_tgba_lacim() LTL translation 4446 algorithm. Historically, this TGBA implementation and LTL 4447 translation were the first to be implemented in Spot (by 4448 mistake!) and this resulted in many bad design decisions. In 4449 practice they were of no use as we only work with explicit 4450 automata (i.e. not symbolic) in Spot, and those produced by 4451 these techniques are simply too big. 4452 4453 - All support for ELTL, i.e., LTL logic extended with operators 4454 represented by automata has been removed. It was never used in 4455 practice because it had no practical user interface, and the 4456 translation was a purely-based BDD encoding producing huge 4457 automata (when viewed explictely), using the above and non 4458 longuer supported tgba_bdd_concrete class. 4459 4460 - Our implementation of the Kupferman-Vardi complementation has 4461 been removed: it was unused in practice beause of the size of 4462 the automata built, and it did not survive the conversion of 4463 acceptance sets from BDDs to bitsets. 4464 4465 - The unused implementation of state-based alternating Büchi 4466 automata has been removed. 4467 4468 - Input and output in the old, Spot-specific, text format for 4469 TGBA, has been fully removed. We now use HOA everywhere. (In 4470 case you have a file in this format, install Spot 1.2.6 and use 4471 "src/tgbatest/ltl2tgba -H -X file" to convert the file to HOA.) 4472 4473New in spot 1.2.6 (2014-12-06) 4474 4475 * New features: 4476 4477 - ltlcross --verbose is a new option to see what is being done 4478 4479 * Bug fixes: 4480 4481 - Remove one incorrect simplification rule for PSL discovered 4482 via checks on random formulaes. (The bug was very unlikely 4483 to trigger on non-random formulas, because it requires a SERE 4484 with an entire subexpression that is unsatisfiable.) 4485 - When the automaton resulting from the translation of a positive 4486 formula is deterministic, ltlcross will compute its complement 4487 to perform additional checks against other translations of the 4488 positive formula. The same procedure should be performed with 4489 automata obtained from negated formulas, but because of a typo 4490 this was not the case. 4491 - the neverclaim parser will now diagnose redefinitions of 4492 state labels. 4493 - the acceptance specification in the HOA format output have been 4494 adjusted to match recent changes in the format specifications. 4495 - atomic propositions are correctly escaped in the HOA output. 4496 - the build rules for documentation have been made compatible with 4497 version 8.0 of Org-mode. (This was only a problem if you build 4498 from the git repository, or if you want to edit the 4499 documentation.) 4500 - recent to changes to libstd++ (as shipped by g++ 4.9.2) have 4501 demonstrated that the order of transitions output by the 4502 LTL->TGBA translation used to be dependent on the implementation 4503 of the STL. This is now fixed. 4504 - some developpement version of libstd++ had a bug (PR 63698) in 4505 the assignment of std::set, and that was triggered in two places 4506 in Spot. The workaround (not assigning sets) is actually more 4507 efficient, so we can consider it as a bug fix, even though 4508 libstd++ has also been fixed. 4509 - all parsers would report wrong line numbers while processing 4510 files with DOS style newlines. 4511 - add support for SWIG 3.0. 4512 4513New in spot 1.2.5 (2014-08-21) 4514 4515 * New features: 4516 4517 - The online ltl2tgba translator will automatically attempt to 4518 parse a formula using LBT's syntax if it cannot parse it using 4519 the normal infix syntax. It also has an option to display 4520 formulas using LBT's syntax. 4521 4522 - ltl2tgba and dstar2tgba have a new experimental option --hoaf to 4523 output automata in the Hanoï Omega Automaton Format whose 4524 current draft is at http://adl.github.io/hoaf/ 4525 The corresponding C++ function is spot::hoaf_reachable() in 4526 tgbaalgos/hoaf.hh. 4527 4528 - 'randltl 4' is now a shorthand for 'randltl p0 p1 p2 p3'. 4529 4530 - ltlcross has a new option --save-bogus=FILENAME to save any 4531 formula for which a problem (other than timeout) was detected 4532 during translation or using the resulting automatas. 4533 4534 * Documentation: 4535 4536 - The man page for ltl2tgba has some new notes and references 4537 about TGBA and about monitors. 4538 4539 * Bug fixes: 4540 4541 - Fix incorrect simplification of promises in the translation 4542 of the M operator (you may suffer from the bug even if you do 4543 not use this operator as some LTL patterns are automatically 4544 reduced to it). 4545 - Fix simplification of bounded repetition in SERE formulas. 4546 - Fix incorrect translation of PSL formulas of the form !{f} where 4547 f is unsatisifable. A similar bug was fixed for {f} in Spot 4548 1.1.4, but for some reason it was not fixed for !{f}. 4549 - Fix parsing of neverclaims produced by Modella. 4550 - Fix a memory leak in the little-used conversion from 4551 transition-based alternating automata to tgba. 4552 - Fix a harmless uninitialized read in BuDDy. 4553 - When writing to the terminal, ltlcross used to display each 4554 formula in bright white, to make them stand out. It turns out 4555 this was actually hiding the formulas for people using a 4556 terminal with white background... This version displays formula 4557 in bright blue instead. 4558 - 'randltl -n -1 --seed 0' and 'randltl -n -1 --seed 1' used to 4559 generate nearly the same list of formulas, shifted by one, 4560 because the PRNG write reset with an incremented seed between 4561 each output formula. The PRNG is now reset only once. 4562 4563New in spot 1.2.4 (2014-05-15) 4564 4565 * New features: 4566 4567 - "-B -x degen-lskip" can be used to disable level-skipping in the 4568 degeralization procedure called by ltl2tgba and dstar2tgba. 4569 This is mostly meant for running experiments. 4570 - "-B -x degen-lcache=N" can be used to experiment with different 4571 type of level caching during degeneralization. 4572 4573 * Bug fixes: 4574 4575 - Change the Python bindings to make them compatible with Swig 3.0. 4576 - "ltl2tgta --ta" could crash in certain conditions due to the 4577 introduction of a simulation-based reduction after 4578 degeneralization. 4579 - Fix four incorrect formula-simplification rules, three were 4580 related to the factorization of Boolean subformulas in 4581 operands of the non-length-matching "&" SERE operator, and 4582 a fourth one could only be enabled by explicitely passing the 4583 favor_event_univ option to the simplifier (not the default). 4584 - Fix incorrect translation of the fusion operator (":") in SERE 4585 such as {xx;1}:yy[*] where the left operand has 1 as tail. 4586 4587New in spot 1.2.3 (2014-02-11) 4588 4589 * New features: 4590 4591 - The SPOT_SATLOG environment variable can be set to a filename to 4592 obtain statistics about the different iterations of the 4593 SAT-based minimization. For an example, see 4594 http://spot.lrde.epita.fr/satmin.html 4595 - The bench/dtgbasat/ benchmark has been updated to use SPOT_SATLOG 4596 and record more statistics. 4597 - The default value for the SPOT_SATSOLVER environment 4598 variable has been changed to "glucose -verb=0 -model %I >%O". 4599 This assumes that glucose 3.0 is installed. For older 4600 versions of glucose, remove the "-model" option. 4601 4602 * Bug fixes: 4603 4604 - More fixes for Python 3 compatibility. 4605 - Fix calculation of length_boolone(), were 'Xa|b|c' was 4606 considered as length 6 instead of 4 (because it is 'Xa|(b|a)' 4607 were (b|a) is Boolean). 4608 - Fix Clang-3.5 warnings. 4609 - randltl -S did not honor --boolean-priorities. 4610 - randltl had trouble generating formulas when all unary, or 4611 all binary/n-ary operators were disabled. 4612 - Fix spurious testsuite failure when using Pandas 0.13. 4613 - Add the time spent in child processes when measuring time 4614 with the timer class. 4615 - Fix determinism of the SAT-based minimization encoding. 4616 (It would sometimes produce different equivalent automata, 4617 because of a different encoding order.) 4618 - If the SAT-based minimization is asked for a 10-state automaton 4619 and returns a 6-state automaton, do not ask for a 9-state 4620 automaton in the next iteration... 4621 - Fix some compilation issue with the version of Apple's Clang 4622 that is installed with MacOS X 10.9. 4623 - Fix VPATH builds when building from the git repository. 4624 - Fix UP links in the html documentation for command-line tools. 4625 4626New in spot 1.2.2 (2014-01-24) 4627 4628 * Bug fixes: 4629 4630 - Fix compilation *and* behavior of bitvectors on 32-bit 4631 architectures. 4632 - Fix some compilation errors observed using the antique G++ 4.0.1. 4633 - Fix compatibility with Python 3 in the test suite. 4634 - Fix a couple of new clang warnings (like "unused private member"). 4635 - Add some missing #includes that are not included indirectly 4636 when the C++ compiler is in C++11 mode. 4637 - Fix detection of numbers that are too large in the ELTL parser. 4638 - Fix a memory leak in the ELTL parser, and avoid some unnecessary 4639 calls to strlen() at the same time. 4640 4641New in spot 1.2.1 (2013-12-11) 4642 4643 * New features: 4644 4645 - commands for translators specified to ltlcross can now 4646 be given "short names" to be used in the CSV or JSON output. 4647 For instance 4648 ltlcross '{small} ltl2tgba -s --small %f >%N' ... 4649 will run the command "ltl2tgba -s --small %f >%N", but only 4650 print "small" in output files. 4651 4652 - ltlcross' CSV and JSON output now contains two additional 4653 columns: exit_status and exit_code, used to report failures of 4654 the translator. If the translation failed, only the time is 4655 reported, and the rest of the statistics, which are missing, 4656 area left empty (in CVS) or null (in JSON). A new option, 4657 --omit-missing can be used to remove lines for failed 4658 translations, and remove these two columns. 4659 4660 - if ltlcross is used with --products=+5 instead of --products=5 4661 then the stastics for each of the five products will be output 4662 separately instead of being averaged. 4663 4664 - if ltlcross is used with tools that produce deterministic Streett 4665 or Rabin automata (as specified with %D), then the statistics 4666 output in CSV or JSON will have some extra columns to report 4667 the size of these input automata before ltlcross converts them 4668 into TGBA to perform its regular checks. 4669 4670 - ltlfilt, ltl2tgba, ltl2tgta, and ltlcross can now read formulas 4671 from CSV files. Use option -F FILE/COL to read formulas from 4672 column COL of FILE. Use -F FILE/-COL if the first line of 4673 FILE be ignored. 4674 4675 - when ltlfilt processes formulas from a CSV file, it will output 4676 each CSV line whose formula matches the given constraints, with 4677 the rewriten formula. The new escape sequence %< (text in 4678 columns before the formula) and %> (text after) can be used 4679 with the --format option to alter this output. 4680 4681 - ltlfilt, genltl, randltl, and ltl2tgba have a --csv-escape option 4682 to help escape formulas in CSV files. 4683 4684 - Please check 4685 http://spot.lrde.epita.fr/csv.html 4686 for some discussion and examples of the last few features. 4687 4688 * Bug fixes: 4689 4690 - ltlcross' CSV output has been changed to be more RFC 4180 4691 compliant: it no longuer output useless cosmetic spaces, and 4692 use double-quotes with proper escaping for strings. The only 4693 RFC 4180 rule that it does not follow is that it will terminate 4694 lines with \n instead of \r\n because the latter cause issues 4695 with a couple of tools. 4696 4697 - ltlcross failed to report missing input or output escape sequences 4698 on all but the first configured translator. 4699 4700New in spot 1.2 (2013-10-01) 4701 4702 * Changes to command-line tools: 4703 4704 - ltlcross has a new option --color to color its output. It is 4705 enabled by default when the output is a terminal. 4706 4707 - ltlcross will give an example of infinite word accepted by the 4708 two automata when the product between a positive automaton and a 4709 negative automaton is non-empty. 4710 4711 - ltlcross can now read the Rabin and Streett automata output by 4712 ltl2dstar. This type of output should be specified using '%D': 4713 4714 ltlcross 'ltl2dstar --ltl2nba=spin:path/to/ltl2tgba@-s %L %D' 4715 4716 However because Spot only supports Büchi acceptance, these Rabin 4717 and Streett automata are immediately converted to TGBAs before 4718 further processing by ltlcross. This is still interesting to 4719 search for bugs in translators to Rabin or Streett automata, but 4720 the statistics (of the resulting TGBAs) might not be very relevant. 4721 4722 - When ltlcross obtains a deterministic automaton from a 4723 translator it will now complement this automaton to perform 4724 additional intersection checks. This is complementation is done 4725 only for deterministic automata (because that is cheap) and can 4726 be disabled with --no-complement. 4727 4728 - To help with debugging problems detected by ltlcross, the 4729 environment variables SPOT_TMPDIR and SPOT_TMPKEEP control where 4730 temporary files are created and if they should be erased. Read 4731 the man page of ltlcross for details. 4732 4733 - There is a new command, named dstar2tgba, that converts a 4734 deterministic Rabin or Streett automaton (expressed in the 4735 output format of ltl2dstar) into a TGBA, BA or Monitor. 4736 4737 In the case of Rabin acceptance, the conversion will output a 4738 deterministic Büchi automaton if one such automaton exist. Even 4739 if no such automaton exists, the conversion will actually 4740 preserves the determinism of any SCC that can be kept 4741 deterministic. 4742 4743 In the case of Streett acceptance, the conversion produces 4744 non-deterministic Büchi automata with Generalized acceptance. 4745 These are then degeneralized if requested. 4746 4747 See http://spot.lrde.epita.fr/dstar2tgba.html for some 4748 examples, and the man page for more reference. 4749 4750 - The %S escape sequence used by ltl2tgba --stats to display the 4751 number of SCCs in the output automaton has been renamed to %c. 4752 This makes it more homogeneous with the --stats option of the 4753 new dstar2tgba command. 4754 4755 Additionally, the %p escape can now be used to show whether the 4756 output automaton is complete, and the %r escape will give the 4757 number of seconds spent building the output automaton (excluding 4758 the time spent parsing the input). 4759 4760 - ltl2tgba, ltl2tgta, and dstar2tgba have a --complete option 4761 to output complete automata. 4762 4763 - ltl2tgba, ltl2tgta, and dstar2tgba can use a SAT-solver to 4764 minimize deterministic automata. Doing so is only needed on 4765 properties that are stronger than obligations (for obligations 4766 our WDBA-minimization procedure will return a minimimal 4767 deterministic automaton more efficiently) and is disabled by 4768 default. See the spot-x(7) man page for documentation about the 4769 related options: sat-minimize, sat-states, sat-acc, state-based. 4770 See also http://spot.lrde.epita.fr/satmin.html for some 4771 examples. 4772 4773 - ltlfilt, genltl, and randltl now have a --latex option to output 4774 formulas in a way that its easier to embed in a LaTeX document. 4775 Each operator is output as a command such as \U, \F, etc. 4776 doc/tl/spotltl.sty gives one possible definition for each macro. 4777 4778 - ltlfilt, genltl, and randltl have a new --format option to 4779 indicate how to present the output formula, possibly with 4780 information about the input. 4781 4782 - ltlfilt as a new option, --relabel-bool, to abstract independent 4783 Boolean subformulae as if they were atomic propositions. 4784 For instance "a & GF(c | d) & b & X(c | d)" would be rewritten 4785 as "p0 & GF(p1) & Xp1". 4786 4787 * New functions and classes in the library: 4788 4789 - dtba_sat_synthetize(): Use a SAT-solver to build an equivalent 4790 deterministic TBA with a fixed number of states. 4791 4792 - dtba_sat_minimize(), dtba_sat_minimize_dichotomy(): Iterate 4793 dtba_sat_synthetize() to reduce the number of states of a TBA. 4794 4795 - dtgba_sat_synthetize(), dtgba_sat_minimize(), 4796 dtgba_sat_minimize_dichotomy(): Likewise, for deterministic TGBA. 4797 4798 - is_complete(): Check whether a TGBA is complete. 4799 4800 - tgba_complete(): Complete an automaton by adding a sink state 4801 if needed. 4802 4803 - dtgba_complement(): Complement a deterministic TGBA. 4804 4805 - satsolver(): Run an (external) SAT solver, honoring the 4806 SPOT_SATSOLVER environment variable if set. 4807 4808 - tba_determinize(): Run a power-set construction, and attempt 4809 to fix the acceptance simulation to build a deterministic TBA. 4810 4811 - dstar_parse(): Read a Streett or Rabin automaton in 4812 ltl2dstar's format. Note that this format allows only 4813 deterministic automata. 4814 4815 - nra_to_nba(): Convert a (possibly non-deterministic) Rabin 4816 automaton to a non-deterministic Büchi automaton. 4817 4818 - dra_to_ba(): Convert a deterministic Rabin automaton to a Büchi 4819 automaton, preserving acceptance in all SCCs where this is possible. 4820 4821 - nsa_to_tgba(): Convert a (possibly non-deterministic) Streett 4822 automaton to a non-deterministic TGBA. 4823 4824 - dstar_to_tgba(): Convert any automaton returned by dstar_parse() 4825 into a TGBA. 4826 4827 - build_tgba_mask_keep(): Build a masked TGBA that shows only 4828 a subset of states of another TGBA. 4829 4830 - build_tgba_mask_ignore(): Build a masked TGBA that ignore 4831 a subset of states of another TGBA. 4832 4833 - class tgba_proxy: Helps writing on-the-fly algorithms that 4834 delegate most of their methods to the original automaton. 4835 4836 - class bitvect: A dynamic bit vector implementation. 4837 4838 - class word: An infinite word, stored as prefix + cycle, with a 4839 simplify() methods to simplify cycle and prefix in obvious ways. 4840 4841 - class temporary_file: A temporary file. Can be instanciated with 4842 create_tmp_file() or create_open_tmpfile(). 4843 4844 - count_state(): Return the number of states of a TGBA. Implement 4845 a couple of specializations for classes where is can be know 4846 without exploration. 4847 4848 - to_latex_string(): Output a formula using LaTeX syntax. 4849 4850 - relabel_bse(): Relabeling of Boolean Sub-Expressions. 4851 Implements ltlfilt's --relabel-bool option describe above. 4852 4853 * Noteworthy internal changes: 4854 4855 - When minimize_obligation() is not given the formula associated 4856 to the input automaton, but that automaton is deterministic, it 4857 can still attempt to call minimize_wdba() and check the correcteness 4858 using dtgba_complement(). This allows dstar2tgba to apply 4859 WDBA-minimization on deterministic Rabin automata. 4860 4861 - tgba_reachable_iterator_depth_first has been redesigned to 4862 effectively perform a DFS. As a consequence, it does not 4863 inherit from tgba_reachable_iterator anymore. 4864 4865 - postproc::set_pref() was used to accept an argument among Any, 4866 Small or Deterministic. These can now be combined with Complete 4867 as Any|Complete, Small|Complete, or Deterministic|Complete. 4868 4869 - operands of n-ary operators (like & and |) are now ordered so 4870 that Boolean terms come first. This speeds up syntactic 4871 implication checks slightly. Also, literals are now sorted 4872 using strverscmp(), so that p5 comes before p12. 4873 4874 - Syntactic implication checks have been generalized slightly 4875 (for instance 'a & b & F(a & b)' is now reduced to 'a & b' 4876 while it was not changed in previous versions). 4877 4878 - All the parsers implemented in Spot now use the same type to 4879 store locations. 4880 4881 - Cleanup of exported symbols 4882 4883 All symbols in the library now have hidden visibility on ELF systems. 4884 Public classes and functions have been marked explicitely for export 4885 with the SPOT_API macro. 4886 4887 During this massive update, some of functions that should not have 4888 been made public in the first place have been moved away so that 4889 they can only be used from the library. Some old of unused 4890 functions have been removed. 4891 4892 removed: 4893 - class loopless_modular_mixed_radix_gray_code 4894 4895 hidden: 4896 - class acc_compl 4897 - class acceptance_convertor 4898 - class bdd_allocator 4899 - class free_list 4900 4901 * Bug fixes: 4902 4903 - Degeneralization was not indempotant on automata with an 4904 accepting initial state that was on a cycle, but without 4905 self-loop. 4906 4907 - Configuring with --enable-optimization would reset the value of 4908 CXXFLAGS. 4909 4910 4911New in spot 1.1.4 (2013-07-29) 4912 4913 * Bug fixes: 4914 - The parser for neverclaim, updated in 1.1.3, would fail to 4915 parse guards of the form (a) || (b) output by ltl2ba or 4916 ltl3ba, and would only understand ((a) || (b)). 4917 - When used from ltlcross, the same parser would fail to 4918 parse further neverclaims after the first failure. 4919 - Add a missing newline in some error message of ltlcross. 4920 - Expressions like {SERE} were wrongly translated and simplified 4921 for SEREs that accept the empty word: they were wrongly reduced 4922 to true. Simplification and translation rules have been fixed, 4923 and the doc/tl/tl.pdf specifications have been updated to better 4924 explain that {SERE} has the semantics of a closure operator that 4925 is not exactly what one could expect after reading the PSL 4926 standard. 4927 - Various typos. 4928 4929New in spot 1.1.3 (2013-07-09) 4930 4931 * New feature: 4932 - The neverclaim parser now understands the new style of output 4933 used by Spin 6.24 and later. 4934 * Bug fixes: 4935 - The scc_filter() function could abort with a BDD error. If all 4936 the acceptance sets of an SCC but the first one were useless. 4937 - The script in bench/spin13/ would not work on MacOS X because 4938 of some non-portable command. 4939 - A memory corruption in ltlcross. 4940 4941New in spot 1.1.2 (2013-06-09) 4942 4943 * Bug fixes: 4944 - Uninitialized variables in ltlcross (affect the count of terminal 4945 weak, and strong SCCs). 4946 - Workaround an old GCC bug to allow compilation with g++ <= 4.5 4947 - Fix several Doxygen comments so that they display correctly. 4948 4949New in spot 1.1.1 (2013-05-13): 4950 4951 * New features: 4952 4953 - lbtt_reachable(), the function that outputs a TGBA in LBTT's 4954 format, has a new option to indicate that the TGBA being printed 4955 is in fact a Büchi automaton. In this case it outputs an LBTT 4956 automaton with state-based acceptance. 4957 4958 The output of the guards has also been changed in two ways: 4959 1. atomic propositions that do not match p[0-9]+ are always 4960 double-quoted. This avoids issues where t or f were used as 4961 atomic propositions in the formula, output as-is in the 4962 automaton, and read back as true or false. Other names that 4963 correspond to LBT operators would cause problem as well. 4964 2. formulas that label transitions are now output as 4965 irredundant-sums-of-products. 4966 4967 - 'ltl2tgba --ba --lbtt' will now output automata with state-based 4968 acceptance. You can use 'ltl2tgba --ba --lbtt=t' to force the 4969 output of transition-based acceptance like in the previous 4970 versions. 4971 4972 Some illustrations of this point and the previous one can be 4973 found in the man page for ltl2tgba(1). 4974 4975 - There is a new function scc_filter_states() that removes all 4976 useless states from a TGBA. It is actually an abbridged version 4977 of scc_filter() that does not alter the acceptance conditions of 4978 the automaton. scc_filter_state() should be used when 4979 post-processing TGBAs that actually represent BAs. 4980 4981 - simulation_sba(), cosimulation_sba(), and 4982 iterated_simulations_sba() are new functions that apply to TGBAs 4983 that actually represent BAs. They preserve the imporant 4984 property that if a state of the BA is is accepting, the outgoing 4985 transitions of that state are all accepting in the TGBA that 4986 represent the BA. This is something that was not preserved by 4987 functions cosimultion() and iterated_simulations() as mentionned 4988 in the bug fixes below. 4989 4990 - ltlcross has a new option --seed, that makes it possible to 4991 change the seed used by the random graph generator. 4992 4993 - ltlcross has a new option --products=N to check the result of 4994 each translation against N different state spaces, and everage 4995 the statistics of these N products. N default to 1; larger 4996 values increase the chances to detect inconsistencies in the 4997 translations, and also make the average size of the product 4998 built against the translated automata a more pertinent 4999 statistic. 5000 5001 - bdd_dict::unregister_all_typed_variables() is a new function, 5002 making it easy to unregister all BDD variables of a given type 5003 owned by some object. 5004 5005 * Bug fixes: 5006 5007 - genltl --gh-r generated the wrong formulas due to a typo. 5008 - ltlfilt --eventual and --universal were not handled properly. 5009 - ltlfilt --stutter-invariant would trigger an assert on PSL formulas. 5010 - ltl2tgba, ltl2tgta, ltlcross, and ltlfilt, would all choke on empty 5011 lines in a file of formulas. They now ignore empty lines. 5012 - The iterated simulation applied on degeneralized TGBA was bogus 5013 for two reasons: one was that cosimulation was applied using the 5014 generic cosimulation for TGBA, and the second is that 5015 SCC-filtering, performed between iterations, was also a 5016 TGBA-based algorithm. Both of these algorithms could lose the 5017 property that if a TGBA represents a BA, all the outgoing 5018 transitions of a state should be accepting. As a consequence, some 5019 formulas where translated to incorrect Büchi automata. 5020 5021New in spot 1.1 (2013-04-28): 5022 5023 Several of the new features described below are discribed in 5024 5025 Tomáš Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmír 5026 Křetínský, Jan Strejček: Compositional Approach to Suspension and 5027 Other Improvements to LTL Translation. To appear in the 5028 proceedings of SPIN'13. 5029 5030 * New features in the library: 5031 5032 - The postprocessor class now takes an optional option_map 5033 argument that can be used to specify fine-tuning options, making 5034 it easier to benchmark different scenarios while developing new 5035 postprocessings. 5036 5037 - A new translator class implements a complete translation chain, 5038 from LTL/PSL to TGBA/BA/Monitor. It performs pre- and 5039 post-processings in addition to the core translation, and offers 5040 an interface similar to that used in the postprocessor class, to 5041 specify the intent of the translation. 5042 5043 - The degeneralization algorithm has learned three new tricks: 5044 level reset, level caching, and SCC-based ordering. The former 5045 two are enabled by default. Benchmarking has shown that the 5046 latter one does not always have a positive effect, so it is 5047 disabled by default. (See SPIN'13 paper.) 5048 5049 - The scc_filter() function, which removes dead SCCs and also 5050 simplify acceptance conditions, has learnt how to simplify 5051 acceptance conditions in a few tricky situations that were not 5052 simplified previously. (See SPIN'13 paper.) 5053 5054 - A new translation, called compsusp(), for "Compositional 5055 Suspension" is implemented on top of ltl_to_tgba_fm(). 5056 (See SPIN'13 paper.) 5057 5058 - Some experimental LTL rewriting rules that trie to gather 5059 suspendable formulas are implemented and can be activated 5060 with the favor_event_univ option of ltl_simplifier. As 5061 always please check doc/tl/tl.tex for the list of rules. 5062 5063 - An experimental "don't care" (direct) simulation has been 5064 implemented. This simulations consider the acceptance 5065 of out-of-SCC transitions as "don't care". It is not 5066 enabled by default because it currently is very slow. 5067 5068 - remove_x() is a function that take a formula, and rewrite it 5069 without the X operator. The rewriting is only correct for 5070 stutter-insensitive LTL formulas (See K. Etessami's paper in IFP 5071 vol. 75(6). 2000) This algorithm is accessible from the 5072 command-line using ltlfilt's --remove-x option. 5073 5074 - is_stutter_insensitive() takes any LTL formula, and check 5075 whether it is stutter-insensitive. This algorithm is accessible 5076 from the command-line using ltlfilt's --stutter-insensitive 5077 option. 5078 5079 - Several functions have been introduced to check the 5080 strength of an SCC. 5081 is_inherently_weak_scc() 5082 is_weak_scc() 5083 is_syntactic_weak_scc() 5084 is_complete_scc() 5085 is_terminal_scc() 5086 is_syntactic_terminal_scc() 5087 5088 Beware that the costly is_weak_scc() function introduced in Spot 5089 1.0, which is based on a cycle enumeration, has been renammed to 5090 is_inherently_weak_scc() to match established vocabulary. 5091 5092 * Command-line tools: 5093 5094 - ltl2tgba and ltl2tgta now honor a new --extra-options (or -x) 5095 flag to fine-tune the algorithms used. The available options 5096 are documented in the spot-x (7) manpage. For instance use '-x 5097 comp-susp' to use the afore-mentioned compositional suspension. 5098 5099 - The output format of 'ltlcross --json' has been changed slightly. 5100 In a future version we will offer some reporting script that turn 5101 such JSON output into various tables and graphs, and these change 5102 are required to make the format usable for other benchmarks (not 5103 just ltlcross). 5104 5105 - ltlcross will now count the number of non-accepting, terminal, 5106 weak, and strong SCCs, as well as the number of terminal, weak, 5107 and strong automata produced by each tool. 5108 5109 * Documentation: 5110 5111 - org-mode files used to generate the documentation about 5112 command-line tools (shown at http://spot.lrde.epita.fr/tools.html) 5113 is distributed in doc/org/. The resulting html files are also 5114 in doc/userdoc/. 5115 5116 * Web interface: 5117 5118 - A new "Compositional Suspension" tab has been added to experiment 5119 with compositional suspension. 5120 5121 * Benchmarks: 5122 5123 - See bench/spin13/README for instructions to reproduce our Spin'13 5124 benchmark for the compositional suspension. 5125 5126 * Bug fixes: 5127 5128 - There was a memory leak in the LTL simplification code, that could 5129 only be triggered when disabling advanced simplifications. 5130 5131 - The translation of the PSL formula !{xxx} was incorrect when xxx 5132 simplified to false. 5133 5134 - Various warnings triggered by new compilers. 5135 5136New in spot 1.0.2 (2013-03-06): 5137 5138 * New features: 5139 - the on-line ltl2tgba.html interface can output deterministic or 5140 non-deterministic monitors. However, and unlike the ltl2tgba 5141 command-line tool, it doesn't different output formats. 5142 - the class ltl::ltl_simplifier now has an option to rewrite Boolean 5143 subformulaes as irredundante-sum-of-product during the simplification 5144 of any LTL/PSL formula. The service is also available as a method 5145 ltl_simplifier::boolean_to_isop() that applies this rewriting 5146 to a Boolean formula and implements a cache. 5147 ltlfilt as a new option --boolean-to-isop to try to apply the 5148 above rewriting from the command-line: 5149 % ltlfilt --boolean-to-isop -f 'GF((a->b)&(b->c))' 5150 GF((!a & !b) | (b & c)) 5151 This is currently not used anywhere else in the library. 5152 * Bug fixes: 5153 - 'ltl2tgba --high' is documented to be the same as 'ltl2tgba', 5154 but by default ltl2tgba forgot to enable LTL simplifications based 5155 on language containment, which --high do enable. There are now 5156 enabled by default. 5157 - the on-line ltl2tgba.html interface failed to output monitors, 5158 testing automata, and generalized testing automata due to two 5159 issues with the Python bindings. It also used to display 5160 Testing Automaton Options when the desired output was set to Monitor. 5161 - bench/ltl2tgba would not work in a VPATH build. 5162 - a typo caused some .dir-locals.el configuration parameters to be 5163 silently ignored by emacs 5164 - improved Doxygen comments for formula_to_bdd, bdd_to_formula, 5165 and bdd_dict. 5166 - src/tgbatest/ltl2tgba (not to be confused with src/bin/ltl2tgba) 5167 would have a memory leak when passed the conflicting option -M 5168 and -O. It probably has many other problems. Do not use 5169 src/tgbatest/ltl2tgba if you are not writing a test case for 5170 Spot. Use src/bin/ltl2tgba instead. 5171 5172New in spot 1.0.1 (2013-01-23): 5173 5174 * Bug fixes: 5175 - Two executions of the simulation reductions could produce 5176 two isomorphic automata, but with transitions in a different 5177 order. 5178 - ltlcross did not diagnose write errors to temporary files, 5179 and certain versions of g++ would warn about it. 5180 - "P0.init" is parsed as an atomic even without the double quotes, 5181 but it was always output with double quotes. This version will 5182 not quote this atomic proposition anymore. 5183 - "U", "W", "M", "R" were correctly parsed as atomic propositions 5184 (instead of binary operators) when placed in double quotes, but 5185 on output they were output without quotes, making the result 5186 unparsable. 5187 - the to_lbt_string() functions would always output a trailing space. 5188 This is not the case anymore. 5189 - tgba_product::transition_annotation() would segfault when 5190 called in a product against a Kripke structure. 5191 * Minor improvements: 5192 - Four new LTL simplifications rules: 5193 GF(a|Xb) = GF(a|b) 5194 GF(a|Fb) = GF(a|b) 5195 FG(a&Xb) = FG(a&b) 5196 FG(a&Gb) = FG(a&b) 5197 - The on-line version of ltl2tgba now displays edge and 5198 transition counts, just as the ltlcross tool. 5199 - ltlcross will display the number of timeouts at the end 5200 of its execution. 5201 - ltlcross will diagnose tools with missing input or 5202 output %-sequence before attempting to run any of them. 5203 - The parser for LBT's prefix-style LTL formulas will now 5204 read atomic propositions that are not of the form p1, p2... 5205 This makes it possible to process formulas written in 5206 ltl2dstar's syntax. 5207 * Pruning: 5208 - lbtt has been removed from the distribution. A copy of the last 5209 version we distributed is still available at 5210 http://spot.lip6.fr/dl/lbtt-1.2.1a.tar.gz 5211 and our test suite will use it if it is installed, but the same 5212 tests are already performed by ltlcross. 5213 - the bench/ltl2tgba/ benchmark, that used lbtt to compare various 5214 LTL-to-Büchi translators, has been updated to use ltlcross. It 5215 now output summary tables in LaTeX. Support for Modella (no 5216 longer available online), and Wring (requires a too old Perl 5217 version) have been dropped. 5218 - the half-baked and underdocumented "Event TGBA" support in 5219 src/evtgba*/ has been removed, as it was last worked on in 2004. 5220 5221New in spot 1.0 (2012-10-27): 5222 5223 * License change: Spot is now distributed using GPL v3+ instead 5224 of GPL v2+. This is because we started using some third-party 5225 files distributed under GPL v3+. 5226 5227 * Command-line tools 5228 5229 Useful command-line tools are now installed in addition to the 5230 library. Some of these tools were originally written for our test 5231 suite and had evolved organically into useful programs with crappy 5232 interfaces: they have now been rewritten with better argument 5233 parsing, saner defaults, and they come with man pages. 5234 5235 - genltl: Generate LTL formulas from scalable patterns. 5236 This offers 20 patterns so far. 5237 5238 - randltl: Generate random LTL/PSL formulas. 5239 5240 - ltlfilt: Filter lists of formulas according to several criteria 5241 (e.g., match only safety formulas that are larger than 5242 some given size). Besides being used as a "grep" tool 5243 for formulas, this can also be used to convert 5244 files of formulas between different syntaxes, apply 5245 some simplifications, check whether to formulas are 5246 equivalent, ... 5247 5248 - ltl2tgba: Translate LTL/PSL formulas into Büchi automata (TGBA, 5249 BA, or Monitor). A fundamental change to the 5250 interface is that you may now specify the goal of the 5251 translation: do you you favor deterministic or smaller 5252 automata? 5253 5254 - ltl2tgta: Translate LTL/PSL formulas into Testing Automata. 5255 5256 - ltlcross: Compare the output of translators from LTL/PSL to 5257 Büchi automata, to find bug or for benchmarking. This 5258 is essentially a Spot-based reimplementation of LBTT 5259 that supports PSL in addition to LTL, and that can 5260 output more statistics. 5261 5262 An introduction to these tools can be found on-line at 5263 http://spot.lrde.epita.fr/tools.html 5264 5265 The former test versions of genltl and randltl have been removed 5266 from the source tree. The old version of ltl2tgba with its 5267 gazillion options is still in src/tgbatest/ and is meant to be 5268 used for testing only. Although ltlcross is meant to replace 5269 LBTT, we are still using both tools in this release; however this 5270 is likely to be the last release of Spot that redistributes LBTT. 5271 5272 * New features in the Spot library: 5273 5274 - Support for various flavors of Testing Automata. 5275 5276 The flavors are: 5277 + "classical" Testing Automata, as used for instance by 5278 Geldenhuys and Hansen (Spin'06), using Büchi and 5279 livelock acceptance conditions. 5280 + Generalized Testing Automata, extending the previous 5281 with multiple Büchi acceptance sets. 5282 + Transition-based Generalized Testing Automata moving Büchi 5283 acceptance to transitions, and getting rid of livelock 5284 acceptance conditions by expliciting stuttering self-loops. 5285 5286 Supporting algorithms include anything required to run 5287 the automata-theoretic approach using testing automata: 5288 5289 + dedicated synchronized product 5290 + dedicated emptiness-check for TA and GTA, as these 5291 may require two passes because of the two kinds of 5292 acceptance, while a TGTA can be checked for emptiness 5293 with the same one-pass algorithm as a TGBA. 5294 + conversion from a TGBA to any of the above kind, with 5295 options to reduce these automata with bisimulation, 5296 and to produce a BA/GBA that require a single pass 5297 (at the expense of determinism). 5298 + output in dot format for display 5299 5300 A discussion of these automata, part of Ala Eddine BEN SALEM's 5301 PhD work, should appear in ToPNoC VI (LNCS 7400). The web-based 5302 interface and the aforementioned ltl2tgta tool can be used 5303 to build testing automata. 5304 5305 - TGBA can now be reduced by Reverse Simulation (in addition to 5306 the Direct Simulation introduced in 0.9). A function called 5307 iterated_simulations() will alternate direct and reverse 5308 simulations in a loop as long as it diminishes the size of the 5309 automaton. 5310 5311 - The enumerate_cycles class implements the Loizou-Thanisch 5312 algorithm to enumerate elementary cycles in a SCC. As an 5313 example of use, is_weak_scc() will tell whether an SCC is 5314 inherently weak (all its cycles are accepting, or none of them 5315 are). 5316 5317 - parse_lbt() will parse an LTL formula expressed in the prefix 5318 syntax used (at least) by LBT, LBTT and Scheck. 5319 to_lbt_string() can be used to print an LTL formula using this 5320 syntax. 5321 5322 - to_wring_string() can be used to print an LTL formula into 5323 Wring's syntax. 5324 5325 - The LTL/PSL parser now has a lenient mode that can be useful 5326 to interpret atomic proposition with language-specific constructs. 5327 In lenient mode, any (...) or {...} block that cannot be parsed 5328 as formula will be assumed to be an atomic proposition. 5329 For instance the input (a < b) U (process[2]@ok), normally 5330 flagged as a syntax error, is read as "a < b" U "process[2]@ok" 5331 in lenient mode. 5332 5333 - minimize_obligation() has a new option to disable WDBA 5334 minimization it cases it would produce a deterministic automaton 5335 that is bigger than the original TGBA. This can help 5336 choosing between less states or more determinism. 5337 5338 - new functions is_deterministic() and count_nondet_states() 5339 (The count of nondeterministic states is now displayed on 5340 automata generated with the web interface.) 5341 5342 - A new class, "postprocessor", makes it easier to apply 5343 all available simplification algorithms on a TGBA/BA/Monitors. 5344 5345 * Minor changes: 5346 5347 - The '*' operator can (again) be used as an AND in LTL formulas. 5348 This is for compatibility with formula written in Wring's 5349 syntax. However inside SERE it is interpreted as the Kleen 5350 star. 5351 5352 - When printing a formula using Spin's LTL syntax, we don't 5353 double-quote complex atomic propositions (that was not valid 5354 Spin input anyway). For instance F"foo == 2" used to be 5355 output as <>"foo == 2". We now output <>(foo == 2) instead. 5356 The latter syntax is understood by Spin 6. It can be read 5357 back by Spot in lenient mode (see above). 5358 5359 - The gspn-ssp benchmark has been removed. 5360 5361 5362New in spot 0.9.2 (2012-07-02): 5363 5364 * New features to the web interface. 5365 - It can run ltl3ba (Babiak et al., TACAS'12) where available. 5366 - "a loading logo" is displayed when result is not instantaneous. 5367 * Speed improvements: 5368 - The unicity hash table of BuDDy has been separated separated 5369 node table for better cache-friendliness. The resulting speedup 5370 is around 5% on BDD-intensive algorithms. 5371 - A new BDD operation, called bdd_implies() has been added to 5372 BuDDy to check whether one BDD implies another. This benefits 5373 mostly the simulation and degeneralization algorithms of Spot. 5374 - A new offline implementation of the degeneralization (which 5375 had always been performed on-the-fly so far) available. This 5376 especially helps the Safra complementation. 5377 * Bug fixes: 5378 - The CGI script running for ltl2tgba.html will correctly timeout 5379 after 30s when Spot's translation takes more time. 5380 - Applying WDBA-minimization on an automaton generated by the 5381 Couvreur/LaCIM translator could lead to an incorrect automaton 5382 due to a bug in the definition of product with symbolic 5383 automata. 5384 - The Makefile.am of BuDDy, LBTT, and Spot have been adjusted to 5385 accomodate Automake 1.12 (while still working with 1.11). 5386 - Better error recovery when parsing broken LTL formulae. 5387 - Fix errors and warnings reported by clang 3.1 and the 5388 upcoming g++ 4.8. 5389 5390New in spot 0.9.1 (2012-05-23): 5391 5392 * The version of LBTT we distribute includes a patch from Tomáš 5393 Babiak to count the number of non-deterministic states, and the 5394 number of deterministic automata produced. 5395 See lbtt/NEWS for the list of other differences with the original 5396 version of LBTT 1.2.1. 5397 * The Couvreur/FM translator has learned two new tricks. These only 5398 help to speedup the translation by not issuing states or 5399 acceptance conditions that would be latter suppresed by other 5400 optimizations. 5401 - The translation rules used to translate subformulae of the G 5402 operator have been adjusted not to produce useless loops 5403 already implied by G. This generalizes the "GF" trick 5404 presented in Couvreur's original FM'99 paper. 5405 - Promises generated for formula of the form P(a U (b U c)) 5406 are reduced into P(c), avoiding the introduction of many 5407 promises that imply each other. 5408 * The tgba_parse() function is now available via the Python 5409 bindings. 5410 * Bug fixes: 5411 - The random SERE generator was using the wrong operators 5412 for "and" and "or", mistaking And/Or with AndRat/OrRat. 5413 - The translation of !{r} was incorrect when this subformula 5414 was recurring (e.g. in G!{r}) and r had loops. 5415 - Correctly recognize ltl2tgba's option -rL. 5416 - Using LTL simplification rules based on syntactic implication, 5417 or based on language containment checks, caused BDD variables 5418 to be allocated in an "unnatural" order, resulting in a slower 5419 translation and a less optimal degeneralization. 5420 - When ltl2tgba reads a neverclaim, it now considers the resulting 5421 TGBA as a Büchi automaton, and will display double circles in 5422 the dotty output. 5423 5424New in spot 0.9 (2012-05-09): 5425 5426 * New features: 5427 - Operators from the linear fragment of PSL are supported. This 5428 basically extends LTL with Sequential Extended Regulat 5429 Expressions (SERE), and a couple of operators to bridge SERE and 5430 LTL. See doc/tl/tl.pdf for the list of operators and their 5431 semantics. 5432 - Formula rewritings have been completely revamped, and augmented 5433 with rules for PSL operators (and some new LTL rules as well). 5434 See doc/tl/tl.pdf for the list of the rewritings implemented. 5435 - Some of these rewritings that may produce larger formulas 5436 (for instance to rewrite "{a;b;c}" into "a & X(b & Xc)") 5437 may be explicitely disabled with a new option. 5438 - The src/ltltest/randltl tool can now generate random SEREs 5439 and random PSL formulae. 5440 - Only one translator (ltl2tgba_fm) has been augmented to 5441 translate the new SERE and PSL operators. The internal 5442 translation from SERE to DFA is likely to be rewriten in a 5443 future version. 5444 - A new function, length_boolone(), computes the size of an 5445 LTL/PSL formula while considering that any Boolean term has 5446 length 1. 5447 - The LTL/PSL parser recognizes some UTF-8 characters (like ◇ or 5448 ∧) as operators, and some output routines now have an UTF-8 5449 output mode. Tools like randltl and ltl2tgba have gained an -8 5450 option to enable such output. See doc/tl/tl.pdf for the list 5451 of recognized codepoints. 5452 - A new direct simulation reduction has been implemented. It 5453 works directly on TGBAs. It is in src/tgbaalgos/simlation.hh, 5454 and it can be tested via ltl2tgba's -RDS option. 5455 - unabbreviate_wm() is a function that rewrites the W and M operators 5456 of LTL formulae using R and U. This is called whenever we output 5457 a formula in Spin syntax. By combining this with the aforementioned 5458 PSL rewriting rules, many PSL formulae that use simple SERE can be 5459 converted into LTL formulae that can be feed to tools that only 5460 understand U and R. The web interface will let you do this. 5461 - changes to the on-line translator: 5462 + SVG output is available 5463 + can display some properties of a formula 5464 + new options for direct simulation, larger rewritings, and 5465 utf-8 output 5466 - configure --without-included-lbtt will prevent LBTT from being 5467 configured and built. This helps on systems (such as MinGW) 5468 where LBTT cannot be built. The test-suite will skip any 5469 LBTT-based test if LBTT is missing. 5470 * Interface changes: 5471 - Operators ->, <->, U, W, R, and M are now parsed as 5472 right-associative to better match the PSL standard. 5473 - The constructors for temporal formulae will perform some trivial 5474 simplifications based on associativity, commutativity, 5475 idempotence, and neutral elements. See doc/tl/tl.pdf for the 5476 list of such simplifications. 5477 - Formula instances now have many methods to inspect their 5478 properties (membership to syntactic classes, absence of X 5479 operator, etc...) in constant time. 5480 - LTL/PSL formulae are now handled everywhere as 'const formula*' 5481 and not just 'formula*'. This reflects the true nature of these 5482 (immutable) formula objects, and cleanups a lot of code. 5483 Unfortunately, it is a backward incompatible change: you may have 5484 to add 'const' to a couple of lines in your code, and change 5485 'ltl::const_vistitor' into 'ltl::visitor' if you have written a 5486 custom visitor. 5487 - The new entry point for LTL/PSL simplifications is the function 5488 ltl_simplifier::simplify() declared in src/ltlvisit/simplify.hh. 5489 The ltl_simplifier class implements a cache. 5490 Functions such as reduce() or reduce_tau03() are deprecated. 5491 - The old game-theory-based implementations for direct and delayed 5492 simulation reductions have been removed. The old direct 5493 simulation would only work on degeneralized automata, and yet 5494 produce results inferior to the new direct simulation introduced 5495 in this release. The implementation of delayed simulation was 5496 unreliable. The function reduc_tgba_sim() has been kept 5497 for compatibility (it calls the new direct simulation whatever 5498 the type of simulation requested) and marked as deprecated. 5499 ltl2tgba's options -Rd, -RD are gone. Options -R1t, -R1s, 5500 -R2s, and -R2t are deprecated and all made equivalent to -RDS. 5501 - The tgba_explicit hierarchy has been reorganized in order to 5502 make room for sba_explicit classes that share most of the code. 5503 The main consequence is that the tgba_explicit type no longuer 5504 exists. However the tgba_explicit_number, 5505 tgba_explicit_formula, and tgba_explicit_string still do. 5506 5507New in spot 0.8.3 (2012-03-09): 5508 5509 * Support for both Python 2.x and Python 3.x. 5510 (Previous versions would only work with Python 2.x.) 5511 * The online ltl2tgba.html now stores its state in the URL so that 5512 history is preserved, and links to particular setups can be sent. 5513 * Bug fixes: 5514 - Fix a segfault in the compression code used by the -Z 5515 option of dve2check. 5516 - Fix a race condition in the CGI script. 5517 - Fix a segfault in the CGI script when computing a Büchi run. 5518 5519New in spot 0.8.2 (2012-01-19): 5520 5521 * configure now has a --disable-python option to disable 5522 the compilation of Python bindings. 5523 * Minor speedups in the Safra complementation. 5524 * Better memory management for the on-the-fly degeneralization 5525 algorithm. This mostly benefits to the Safra complementation. 5526 * Bug fixes: 5527 - spot::ltl::length() forgot to count the '&' and '|' operators 5528 in an LTL formula. 5529 - minimize_wdba() could fail to mark some transiant SCCs as accepting, 5530 producing an automaton that was not fully minimized. 5531 - minimize_dfa() could produce incorrect automata, but it is not 5532 clear whether this could have had an inpact on WDBA minimization 5533 (the worse case is that some TGBA would not have been minimized 5534 when they could). 5535 - Fix a Python syntax error in the CGI script. 5536 - Fix compilation with g++ 4.0. 5537 - Fix a make check failure when valgrind is missing. 5538 5539New in spot 0.8.1 (2011-12-18): 5540 5541 * Only bug fixes: 5542 - When ltl2tgba is set to perform both WDBA minimization and 5543 degeneralization, do the latter only if the former failed. 5544 In previous version, automata were (uselessly) degeneralized 5545 before WDBA minimization, causing important slowdowns. 5546 - Fix compilation with Clang 3.0. 5547 - Fix a Makefile setup causing a "make check" failure on MacOS X. 5548 - Fix an mkdir error in the CGI script. 5549 5550New in spot 0.8 (2011-11-28): 5551 5552 * Major new features: 5553 - Spot can read DiVinE models. See iface/dve2/README for details. 5554 - The genltl tool can now output 20 different LTL formula families. 5555 It also replaces the LTLcounter Perl scripts. 5556 - There is a printer and parser for Kripke structures in text format. 5557 * Major interface changes: 5558 - The destructor of all states is now private. Any code that looks like 5559 "delete some_state;" will cause an compile error and should be 5560 updated to "some_state->destroy();". This new syntax is supported 5561 since version 0.7. 5562 - The experimental Nips interface has been removed. 5563 * Minor changes: 5564 - The dotty_reachable() function has a new option "assume_sba" that 5565 can be used for rendering automata with state-based acceptance. 5566 In that case, acceptance states are displayed with a double 5567 circle. ltl2tgba (both command line and on-line) Use it to display 5568 degeneralized automata. 5569 - The dotty_reachable() function will also display transition 5570 annotations (as returned by the tgba::transitition_annotation()). 5571 This can be useful when displaying (small) state spaces. 5572 - Identifiers used to name atomic proposition can contain dots. 5573 E.g.: X.Y is now an atomic proposition, while it was understood 5574 as X&Y in previous versions. 5575 - The Doxygen documentation is no longer built as a PDF file. 5576 * Internal improvements: 5577 - The on-line ltl2tgba CGI script uses a cache to produce faster 5578 answers. 5579 - Better memory management for the states of explicit automata. 5580 Thanks to the aforementioned ->destroy() change, we can avoid 5581 cloning explicit states. 5582 - tgba_product has learned how to be faster when one of the operands 5583 is a Kripke structure (15% speedup). 5584 - The reduction rule for "a M b" has been improved: it can be 5585 reduced to "a & b" if "a" is a pure eventuallity. 5586 - More useless acceptance conditions are removed by SCC simplifications. 5587 * Bug fixes: 5588 - Safra complementation has been fixed in cases where more than 5589 one acceptance conditions where needed to convert the 5590 deterministic Streett automaton as a TGBA. 5591 - The degeneralization is now idempotent. Previously, degeneralizing 5592 an already degeneralized automaton could add some states. 5593 - The degeneralization now has a deterministic behavior. Previously 5594 it was possible to obtain different output depending on the 5595 memory layout. 5596 - Spot now outputs neverclaims with fully parenthesized guards. 5597 I.e., instead of 5598 (!x && y) -> goto S1 5599 it now outputs 5600 ((!(x)) && (y)) -> goto S1 5601 This prevents problems when the model defines `x' as 5602 #define x flag==0 5603 because !x then evaluated to (!flag)==0 instead of !(flag==0). 5604 5605New in spot 0.7.1 (2011-02-07): 5606 5607 * The LTL parser will accept operator ~ (for not) as well 5608 as --> and <--> (for implication and equivalence), allowing 5609 formulae from the Büchi Store to be read directly. 5610 * The neverclaim parser will accept guards of the form 5611 :: !(...) -> goto ... 5612 instead of the more commonly used 5613 :: (!(...)) -> goto ... 5614 This makes it possible to read neverclaims provided by the Büchi Store. 5615 * A new ltl2tgba option, -kt, will count the number of "sub-transitions". 5616 I.e., a transition labelled by "true" counts for 4 "sub-transitions" 5617 if the automaton uses 2 atomic propositions. 5618 * Bugs fixed: 5619 - Fix segfault during WDBA minimization on automata with useless states. 5620 - Use the included BuDDy library if the one already installed 5621 is older than the one distributed with Spot 0.7. 5622 - Fix two typos in the code of the CGI scripts. 5623 5624New in spot 0.7 (2011-02-01): 5625 5626 * Spot is now able to read an automaton expressed as a Spin neverclaim. 5627 * The "experimental" Kripke structure introduced in Spot 0.5 has 5628 been rewritten, and is no longer experimental. We have a 5629 developement version of checkpn using it, and it should be 5630 released shortly after Spot 0.7. 5631 * The function to_spin_string(), that outputs an LTL formula using 5632 Spin's syntax, now takes an optional argument to request 5633 parentheses at all levels. 5634 * src/ltltest/genltl is a new tool that generates some interesting 5635 families of LTL formulae, for testing purpose. 5636 * bench/ltlclasses/ uses the above tool to conduct the same benchmark 5637 as in the DepCoS'09 paper by Cichoń et al. The resulting benchmark 5638 completes in 12min, while it tooks days (or exhausted the memory) 5639 when the paper was written (they used Spot 0.4). 5640 * Degeneralization has again been improved in two ways: 5641 - It will merge degeneralized transitions that can be merged. 5642 - It uses a cache to speed up the improvement introduced in 0.6. 5643 * An implementation of Dax et al.'s paper for minimizing obligation 5644 formulae has been integrated. Use ltl2tgba -Rm to enable this 5645 optimization from the command-line; it will have no effect if the 5646 property is not an obligation. 5647 * bench/wdba/ conducts a benchmark similar to the one on Dax's 5648 webpage, comparing the size of the automata expressing obligation 5649 formula before and after minimization. See bench/wdba/README for 5650 results. 5651 * Using similar code, Spot can now construct deterministic monitors. 5652 * New ltl2tgba options: 5653 -XN: read an input automaton as a neverclaim. 5654 -C, -CR: Compute (and display) a counterexample after running the 5655 emptiness check. With -CR, the counterexample will be 5656 replayed on the automaton to ensure it is correct 5657 (previous version would always compute a replay a 5658 counterexample when emptiness-check was enabled) 5659 -ks: traverse the automaton to compute its number of states and 5660 transitions (this is faster than -k which will also count 5661 SCCs and paths). 5662 -M: Build a deterministic monitor. 5663 -O: Tell whether a formula represents a safety, guarantee, or 5664 obligation property. 5665 -Rm: Minimize automata representing obligation properties. 5666 * The on-line tool to translate LTL formulae into automata 5667 has been rewritten and is now at http://spot.lip6.fr/ltl2tgba.html 5668 It requires a javascript-enabled browser. 5669 * Bug fixes: 5670 - Location of the errors messages in the TGBA parser where inaccurate. 5671 - Various warning fixes for different versions of GCC and Clang. 5672 - The neverclaim output with ltl2tgba -N or -NN used to ignore any 5673 automaton simplification performed after degeneralization. 5674 - The formula simplification based on universality and eventuality 5675 had a quadratic run-time. 5676 5677New in spot 0.6 (2010-04-16): 5678 5679 * Several optimizations to improve some auxiliary steps 5680 of the LTL translation (not the core of the translation): 5681 - Better degeneralization 5682 - SCC simplifications has been tuned for degeneralization 5683 (ltl2tgba now has two options -R3 and -R3f: the latter will 5684 remove every acceptance condition that used to be removed 5685 in Spot 0.5 while the former will leave useless acceptance conditions 5686 going to accepting SCC. Experience shows that -R3 is more 5687 favorable to degeneralization). 5688 - ltl2tgba will perform SCC optimizations before degeneralization 5689 and not the converse 5690 - We added a syntactic simplification rule to rewrite F(a)|F(b) as F(a|b). 5691 We only had a rule for the more specific FG(a)|FG(b) = F(Ga|Gb). 5692 - The syntactic simplification rule for F(a&GF(b)) = F(a)&GF(b) has 5693 be disabled because the latter formula is in fact harder to translate 5694 efficiently. 5695 * New LTL operators: W (weak until) and its dual M (strong release) 5696 - Weak until allows many LTL specification to be specified more 5697 compactly. 5698 - All LTL translation algorithms have been updated to 5699 support these operators. 5700 - Although they do not add any expressive power, translating 5701 "a W b" is more efficient (read smaller output automaton) than 5702 translating the equivalent form using the U operator. 5703 - Basic syntactic rewriting rules will automatically rewrite "a U 5704 (b | G(a))" and "(a U b)|G(a)" as "a W b", so you will benefit 5705 from the new operators even if you do not use them. Similar 5706 rewriting rules exist for R and M, although they are less used. 5707 * New options have been added to the CGI script for 5708 - SVG output 5709 - SCC simplifications 5710 * Bug fixes: 5711 - The precedence of the "->" and "<->" Boolean operators has been 5712 adjusted to better match other tools. 5713 Spot <= 0.5 used to parse "a & b -> c & d" as "a & (b -> c) & d"; 5714 Spot >= 0.6 will parse it as "(a & b) -> (c & d)". 5715 - The random graph generator was fixed (again!) not to produce 5716 dead states as documented. 5717 - Locations in the error messages of the LTL parser were off by one. 5718 5719New in spot 0.5 (2010-02-01): 5720 5721 * We have setup two mailing lists: 5722 - <spot-announce@lrde.epita.fr> is read-only and will be used to 5723 announce new releases. You may subscribe at 5724 https://www.lrde.epita.fr/mailman/listinfo/spot-announce 5725 - <spot@lrde.epita.fr> can be used to discuss anything related 5726 to Spot. You may subscribe at 5727 https://www.lrde.epita.fr/mailman/listinfo/spot-announce 5728 * Two new LTL translations have been implemented: 5729 - eltl_to_tgba_lacim() is a symbolic translation for ELTL based on 5730 Couvreur's LaCIM'00 paper. For this translation (available with 5731 ltl2tgba's option -le), all operators are described as finite 5732 automata. A default set of operators is provided for LTL 5733 (option -lo) and user may add more automaton operators. 5734 - ltl_to_taa() is a translation based on Tauriainen's PhD thesis. 5735 LTL is translated to "self-loop" alternating automata 5736 and then to Transition-based Generalized Automata. (ltl2tgba's 5737 option -taa). 5738 The "Couvreur/FM" translation remains the best LTL translation 5739 available in Spot. 5740 * The data structures used to represent LTL formulae have been 5741 overhauled, and it resulted in a big performence improvement 5742 (in time and memory consumption) for the LTL translation. 5743 * Two complementation algorithms for state-based Büchi automata 5744 have been implemented: 5745 - tgba_kv_complement is an on-the-fly implementation of the 5746 Kupferman-Vardi construction (TCS'05) for generalized acceptance 5747 conditions. 5748 - tgba_safra_complement is an implementation of Safra's 5749 complementation. This algorithm takes a degeneralized Büchi 5750 automaton as input, but our implementation for the Streett->Büchi 5751 step will produce a generalized automaton in the end. 5752 * ltl2tgba has gained several options and the help text has been 5753 reorganized. Please run src/tgbatest/ltl2tgba without arguments 5754 for details. Couvreur/FM is now the default translation. 5755 * The ltl2tgba.py CGI script can now run standalone. It also offers 5756 the Tauriainen/TAA translation, and some options for SCC-based 5757 reductions. 5758 * Automata using BDD-encoded transitions relation can now be pruned 5759 for useless states symbolically using the delete_unaccepting_scc() 5760 function. This is ltl2tgba's -R3b option. 5761 * The SCC-based simplification (ltl2tgba's -R3 option) has been 5762 rewritten and improved. 5763 * The "*" symbol, previously parsed as a synonym for "&" is no 5764 longer recognized. This makes room for an upcoming support of 5765 rational operators. 5766 * More benchmarks in the bench/ directory: 5767 - gspn-ssp/ some benchmarks published at ACSD'07, 5768 - ltlcounter/ translation of a class of LTL formulae used by 5769 Rozier & Vardi at SPIN'07 5770 - scc-stats/ SCC statistics after translation of LTL formulae 5771 - split-product/ parallelizing gain after splitting LTL automata 5772 * An experimental Kripke interface has been developed to simplify 5773 the integration of third party tools that do not use acceptance 5774 conditions and that have label on states instead of transitions. 5775 This interface has not been used yet. 5776 * Experimental interface with the Nips virtual machine. 5777 It is not very useful as Spot isn't able to retrieve any property 5778 information from the model. This will just check assertions. 5779 * Distribution: 5780 - The Boost C++ library is now required. 5781 - Update to Autoconf 2.65, Automake 1.11.1, Libtool 2.2.6b, 5782 Bison 2.4.1, and Swig 1.3.40. 5783 - Thanks to the newest Automake, "make check" will now 5784 run in parallel if you use "make -j2 check" or more. 5785 * Bug fixes: 5786 - Disable warnings from the garbage collection of BuDDy, it 5787 could break the standard output of ltl2tgba. 5788 - Fix several C++ constructs to ensure Spot will build with 5789 GCC 4.3, 4.4, and older 3.x releases, as well as with Intel's 5790 ICC compiler. 5791 - A very old bug in the hash function for LTL formulae caused Spot 5792 to sometimes (but very rarely) consider two different LTL formulae 5793 as equal. 5794 5795New in spot 0.4 (2007-07-17): 5796 5797 * Upgrade to Autoconf 2.61, Automake 1.10, Bison 2.3, and Swig 1.3.31. 5798 * Better LTL simplifications. 5799 * Don't initialize Buddy if it has already been initialized (in case 5800 the client software is already using Buddy). 5801 * Lots of work in the greatspn interface for our ACSD'05 paper. 5802 * Bug fixes: 5803 - Fix the random graph generator not to produce dead states as documented. 5804 - Fix synchronized product in case both side use acceptance conditions. 5805 - Fix some syntax errors with newer versions of GCC. 5806 5807New in spot 0.3 (2006-01-25): 5808 5809 * lbtt 1.2.0 5810 * The CGI script for LTL translation also offers emptiness check algorithms. 5811 * tau03_opt_search implements the "ordering heuristic". 5812 (Submitted by Heikki Tauriainen.) 5813 * A couple of bugs were fixed into the LTL or automata simplifications. 5814 5815New in spot 0.2 (2005-04-08): 5816 5817 * Emptiness checks: 5818 - the new spot::option_map class is used to pass options to 5819 emptiness-check algorithms. 5820 - the new emptiness_check_instantiator class is used to turn a 5821 string such as `algorithm(option1, option2)' into an actual 5822 instance of this emptiness-check algorithm with the given 5823 options. All tools use this. 5824 - tau03_opt_search implements the "condition heuristic". 5825 (Suggested by Heikki Tauriainen.) 5826 * Minor bug fixes. 5827 5828New in spot 0.1 (2005-01-31): 5829 5830 * Emptiness checks: 5831 - They all follow the same interface, and gather statistical data. 5832 - New algorithms: gv04.hh, se05.hh, tau03.hh, tau03opt.hh 5833 - New options for couvreur99: poprem and group. 5834 - reduce_run() try to reduce accepting runs produced by emptiness checks. 5835 - replay_run() ensure accepting runs are actually accepting runs. 5836 * New testing tools: 5837 - ltltest/randltl: Generate random LTL formulae. 5838 - tgbatest/randtgba: Generate random TGBAs. Optionally multiply them 5839 against random LTL formulae. Optionally check them for emptiness 5840 with all available algorithms. Optionally gather statistics. 5841 * bench/emptchk/: Contains scripts that benchmark emptiness-checks. 5842 * Split the degeneralization proxy in two: 5843 - tgba_tba_proxy uses at most max(N,1) copies 5844 - tgba_sba_proxy uses at most 1+max(N,1) copies and has a 5845 state_is_accepting() method 5846 * tgba::transition_annotation annotate a transition with some string. 5847 This comes handy to associate that transition to its high-level name. 5848 * Preliminary support for Event-based GBA (the evtgba*/ directories). 5849 This might as well disappear in a future release. 5850 * LTL formulae are now sorting using their string representation, instead 5851 of their memory address (which is still unique). This makes the output 5852 of the various functions more deterministic. 5853 * The Doxygen documentation is now organized using modules. 5854 5855New in spot 0.0x (2004-08-13): 5856 5857 * New atomic_prop_collect() function: collect atomic propositions 5858 in an LTL formula. 5859 * Fix several typos in documentation, and some warnings in the code. 5860 * Now compiles on Darwin and Cygwin. 5861 * Upgrade to Automake 1.9.1, and lbtt 1.1.2. 5862 (And drop support for older lbtt versions.) 5863 * Support newer versions of Valgrind (>= 2.1.0). 5864 5865New in spot 0.0v (2004-06-29): 5866 5867 * LTL formula simplifications using basic rewriting rules, 5868 a-la Wring syntactic approximations, and Etessami's universal 5869 and existential classes. 5870 - Function reduce() in ltlvisit/reduce.hh is the main interface. 5871 - Can be tested with the CGI script. 5872 * TGBA simplifications using direct simulation, delayed simulation, 5873 and SCC-based simplifications. This is still experimental. 5874 * The LTL parser will now read LTL formulae written using Wring's syntax. 5875 * ltl2tgba_fm() now has options for on-the-fly fair-loop approximations, 5876 and Modella-like branching-postponement. 5877 * GreatSPN interface: 5878 - The `declarative_environment' is now part of Spot itself rather than 5879 part of the interface with GreatSPN. 5880 - the RG and SRG interface can deal with dead markings in three 5881 ways (omit deadlocks from the state graph, stutter on the deadlock 5882 and consider as a regular behavior, or stutter and distinguish the 5883 deadlock with a property). 5884 - update SSP interface to Soheib Baarir latest work. 5885 * Preliminary Python bindings for BuDDy's FDD and BVEC. 5886 * Upgrade to BuDDy 2.3. 5887 5888New in spot 0.0t (2004-04-23): 5889 5890 * `emptiness_check': 5891 - fix two bugs in the computation of the counter example, 5892 - revamp the interface for better customization. 5893 * `never_claim_reachable': new function. 5894 * Introduce annonymous BDD variables in `bdd_dict', and start 5895 to use it in `ltl_to_tgba_fm'. 5896 * Offer never claim in the CGI script. 5897 * Rename EESRG as SSP, and offer specialized variants of the 5898 emptiness_check. 5899 5900New in spot 0.0r (2004-03-08): 5901 5902 * In ltl_to_tgba_fm: 5903 - New option `exprop' to optimize determinism. 5904 - Make the `symbolic indentification' from 0.0p optional. 5905 * `nonacceptant_lbtt_reachable' new function to help getting 5906 accurate statistics from LBTT. 5907 * Revamp the cgi script's user interface. 5908 * Upgrade to lbtt 1.0.3, swig 1.3.21, automake 1.8.3 5909 5910New in spot 0.0p (2004-02-03): 5911 5912 * In ltl_to_tgba_fm: 5913 - identify states with identical symbolic expansions 5914 (i.e., identical continuations) 5915 - use Acc[b] as acceptance condition for Fb, not Acc[Fb]. 5916 * Update and speed-up the cgi script. 5917 * Improve degeneralization. 5918 5919New in spot 0.0n (2004-01-13): 5920 5921 * emptiness_check::check2() is a variant of Couvreur's emptiness check that 5922 explores visited states first. 5923 * Build the EESRG supporting code condinally, as the associated 5924 GreatSPN changes have not yet been contributed to GreatSPN. 5925 * Add a powerset algorithm (determinize TGBA ignoring acceptance 5926 conditions, i.e., as if they were used to recognize finite languages). 5927 * tgba_explicit::merge_transitions: merge transitions with same source, 5928 destination, and acceptance condition. 5929 * Run test cases within valgrind. 5930 * Various bug fixes. 5931 5932New in spot 0.0l (2003-12-01): 5933 5934 * Computation of prime implicants. This simplify the output of 5935 ltl_to_tgba_fm, and allows conditions to be output as some of 5936 product in dot output. 5937 * Optimize translation of GFy in ltl_to_tgba_fm. 5938 * tgba_explicit supports arbitrary binary formulae on transitions 5939 (only conjunctions were allowed). 5940 5941New in spot 0.0j (2003-11-03): 5942 5943 * Use hash_map's instead of map's almost everywhere. 5944 * New emptiness check, based on Couvreur's algorithm. 5945 * LTL propositions can be put inside doublequotes to disambiguate 5946 some constructions. 5947 * Preliminary support for GreatSPN's EESRG. 5948 * Various bug fixes. 5949 5950New in spot 0.0h (2003-08-18): 5951 5952 * More python bindings: 5953 - "import buddy" works (see wrap/python/tests/bddnqueen.py for an example), 5954 - almost all the Spot API is now available via "import spot". 5955 * wrap/python/cgi/ltl2tgba.py is an LTL-to-Büchi translator that 5956 work as as a cgi script. 5957 * Couvreur's FM'99 ltl-to-tgba translation. 5958 5959New in spot 0.0f (2003-08-01): 5960 5961 * More python bindings, still only for the spot::ltl:: namespace. 5962 * Functional GSPN interface. (Enable with --with-gspn=directory.) 5963 * The LTL scanner recognizes /\, \/, and xor. 5964 * Upgrade to lbtt 1.0.2. 5965 * tgba_tba_proxy is an on-the-fly degeneralizer. 5966 * Implements the "magic search" algorithm. 5967 (Works only on a tgba_tba_proxy.) 5968 * Tgba's output algorithms (save(), dotty()) now non-recursive. 5969 * During products, succ_iter will optimize its set of successors 5970 using information computed from the current product state. 5971 * BDD dictionaries are now shared between automata and. This 5972 gets rid of all the BDD-variable translating machinery. 5973 5974New in spot 0.0d (2003-07-13): 5975 5976 * Optimize translation of G operators occurring at the root 5977 of a formula (or its immediate children when the root is a 5978 conjunction). This saves two BDD variables per G operator. 5979 * Distribute lbtt, and run it during `make check'. 5980 * First sketch of GSPN interface. 5981 * succ_iter_concreate::next() completely rewritten. 5982 * Transitions are now labelled by boolean formulae (not only 5983 conjunctions). 5984 * Documentation: 5985 - Output collaboration diagrams. 5986 - Build and distribute PDF manual. 5987 * Many bug fixes. 5988 5989New in spot 0.0b (2003-06-26): 5990 5991 * Everything. 5992