1. 16 Jan, 2021 2 commits
  2. 14 Jan, 2021 3 commits
  3. 12 Jan, 2021 1 commit
    • Alexandre Duret-Lutz's avatar
      require Autoconf 2.69 for building from git · e497ee26
      Alexandre Duret-Lutz authored
      Part of issue #447.
      
      Autoconf 2.69 was released in 2012, so it now widely available.  The
      recent release of 2.70 is obsoleting some constructs, so it will be
      easier on us if we do not have too many versions to support.
      
      * HACKING, configure.ac: Require Autoconf 2.69.
      e497ee26
  4. 11 Jan, 2021 2 commits
  5. 07 Jan, 2021 1 commit
  6. 05 Jan, 2021 3 commits
  7. 18 Dec, 2020 1 commit
    • Alexandre Duret-Lutz's avatar
      bin: add support for -b/--buchi · 8785f5a7
      Alexandre Duret-Lutz authored
      * bin/common_post.cc, bin/randaut.cc: Implement -b/--buchi.
      Also add --sba as alias for -B, and --gba as alias for --tgba.
      * NEWS: Document those changes.
      * doc/org/ltl2tgba.org, doc/org/oaut.org: Adjust documentation.
      * tests/core/ltl2tgba2.test, tests/core/ltlcross2.test,
      tests/core/randaut.test: Add more tests.
      * tests/core/sbacc.test: --sbacc cannot be abbreviated as --sba
      anymore.
      8785f5a7
  8. 16 Dec, 2020 1 commit
  9. 15 Dec, 2020 2 commits
    • Alexandre Duret-Lutz's avatar
      determinize: do not copy the "incomplete" property · 7e2f0918
      Alexandre Duret-Lutz authored
      Mentioned in issue #298.
      
      * spot/twaalgos/determinize.cc: Do not copy prop_complete of
      the input if it is false.
      * tests/python/298.py: Test it.
      * NEWS: Mention the bug.
      7e2f0918
    • Alexandre Duret-Lutz's avatar
      determinize: don't emit colors for temporary braces · f6be0830
      Alexandre Duret-Lutz authored
      Related to issue #298.
      
      * spot/twaalgos/determinize.cc: Recognize braces that are temporary
      to avoid emitting colors when they become empty.
      * tests/python/298.py: New file, showing a reduction of colors.
      * tests/Makefile.am: Add it.
      * tests/core/ltlsynt.test: Adjust expected output (now smaller).
      * tests/core/genltl.test: Adjust one expected output (now larger).
      * NEWS: Mention the issue.
      f6be0830
  10. 14 Dec, 2020 2 commits
  11. 10 Dec, 2020 1 commit
    • Alexandre Duret-Lutz's avatar
      game: rewrite, document, and rename solve_reachability_game · 9a17f567
      Alexandre Duret-Lutz authored
      * spot/twaalgos/game.hh, spot/twaalgos/game.cc: Rename
      solve_reachability_game() as solve_safety_game(), rewrite it (the old
      implementation incorrectly marked dead states as winning for their
      owner).
      * tests/python/paritygame.ipynb: Rename as...
      * tests/python/games.ipynb: ... this, and illustrate
      solve_safety_game().
      * tests/Makefile.am, NEWS, doc/org/tut.org: Adjust.
      * tests/python/except.py: Add more tests.
      9a17f567
  12. 09 Dec, 2020 2 commits
  13. 08 Dec, 2020 4 commits
    • Alexandre Duret-Lutz's avatar
      minimize_wdba: improve handling of terminal automata · 2d6c7ac0
      Alexandre Duret-Lutz authored
      Part of #444.
      
      * spot/twaalgos/minimize.cc (minimize_wdba): Terminal automata do not
      need a product to decide which states are accepting in the DBA.  This
      is faster, and also determinize more formulas of #443.
      * tests/core/ltl2tgba2.test: Adjust the expected iteration where
      determinization will be aborted.
      2d6c7ac0
    • Alexandre Duret-Lutz's avatar
      powerset: deal with accepting sinks more effectively · 48edfd80
      Alexandre Duret-Lutz authored
      Part of #444.
      
      * spot/twaalgos/powerset.cc, spot/twaalgos/powerset.hh: Implement
      accepting sink handling.
      * spot/twaalgos/minimize.cc (minimize_wdba): Pass sinks to
      tgba_powerset.
      * spot/misc/bitvect.hh: Add an interesects method.
      * tests/core/ltl2tgba2.test: More tests.
      * NEWS: Mention this new feature.
      48edfd80
    • Alexandre Duret-Lutz's avatar
      fix ignored aborter in WDBA-minimization · eeaed559
      Alexandre Duret-Lutz authored
      Fixes #443, reported by Roei Nahum.  (However the fix
      only works for the development version, where wdba-det-max
      was introduced to work around that kind of problem.)
      
      * spot/twaalgos/minimize.cc: Avoid aborter being implicitly
      converted to Boolean.
      * tests/core/ltl2tgba2.test: Add test case.
      * THANKS: Add Roei Nahum.
      eeaed559
    • Alexandre Duret-Lutz's avatar
      * NEWS: Typo. · 9da0b3a1
      Alexandre Duret-Lutz authored
      9da0b3a1
  14. 27 Nov, 2020 1 commit
  15. 26 Nov, 2020 2 commits
  16. 25 Nov, 2020 1 commit
  17. 24 Nov, 2020 3 commits
  18. 23 Nov, 2020 1 commit
  19. 19 Nov, 2020 3 commits
  20. 08 Nov, 2020 4 commits