1. 23 Sep, 2020 7 commits
  2. 22 Sep, 2020 2 commits
  3. 19 Sep, 2020 2 commits
  4. 18 Sep, 2020 1 commit
    • Alexandre Duret-Lutz's avatar
      translator: add tls-max-states option · f5965966
      Alexandre Duret-Lutz authored
      This restricts the time spent in translating sub-formulas for
      implication tests by limiting the associated automata to 64 states by
      default.  Doing so this does worsen any test case, and actually remove
      all calls the BuDDy's GC in bdd.test.
      
      * spot/twaalgos/translate.cc, spot/twaalgos/translate.hh,
      spot/tl/simplify.cc, spot/tl/simplify.hh, spot/tl/contain.hh,
      spot/tl/contain.cc, spot/twaalgos/ltl2tgba_fm.cc,
      spot/twaalgos/ltl2tgba_fm.hh: Add support for the option or
      its constraint via an output_aborter.
      * bin/spot-x.cc, NEWS: Document it.
      * tests/core/bdd.test: Adjust and augment test case.
      f5965966
  5. 17 Sep, 2020 1 commit
  6. 16 Sep, 2020 5 commits
  7. 13 Sep, 2020 1 commit
  8. 12 Sep, 2020 1 commit
  9. 10 Sep, 2020 2 commits
  10. 09 Sep, 2020 1 commit
    • Alexandre Duret-Lutz's avatar
      python: add some parity-game bindings · 760bde09
      Alexandre Duret-Lutz authored
      * python/spot/impl.i: Process game.hh.
      * spot/misc/game.cc, spot/misc/game.hh: Make the output of
      parity_game_solve() a solved_game object for easier manipulation in
      Python.
      * bin/ltlsynt.cc: Adjust usage.
      * tests/python/paritygame.ipynb: New file.
      * tests/Makefile.am, doc/org/tut.org: Add it.
      * NEWS: Mention these bindings.
      760bde09
  11. 08 Sep, 2020 4 commits
    • Alexandre Duret-Lutz's avatar
      game: make a propagate_players() function public · 9e8a8429
      Alexandre Duret-Lutz authored
      * bin/ltlsynt.cc (complete_env): Replace this function by...
      * spot/misc/game.hh, spot/misc/game.cc (propagate_players): ... this
      new one, hiding the "state-player" business from ltlsynt.  Also do not
      create a sink states unless necessary.
      * tests/core/ltlsynt.test: Adjust expected number of states.
      9e8a8429
    • Alexandre Duret-Lutz's avatar
      dot: add support for two-player games · 41d088ea
      Alexandre Duret-Lutz authored
      * spot/twaalgos/dot.cc: Honor the "state-player" property and draw
      player 1 states using diamonds.
      * doc/org/hoa.org: Show an example.
      * tests/core/gamehoa.test: Make sure diamond is output.
      * NEWS: Mention this.
      41d088ea
    • Alexandre Duret-Lutz's avatar
      extend HOA I/O to preserve the state-player property · ea9384dd
      Alexandre Duret-Lutz authored
      * spot/parseaut/parseaut.yy, spot/parseaut/scanaut.ll,
      spot/twaalgos/hoa.cc: Add input and output support.
      * doc/org/hoa.org: Document the HOA extension.
      * bin/ltlsynt.cc: Add a --print-game-hoa option to
      produce such format.
      * tests/core/gamehoa.test: New file to test this.
      * tests/Makefile.am: Add it.
      * NEWS: Mention this new feature.
      ea9384dd
    • Alexandre Duret-Lutz's avatar
      game: git rid of the parity_game class · 25c75c55
      Alexandre Duret-Lutz authored
      This class was a simple wrapper on top of twa_graph_ptr, but it's
      easier to simply use a twa_graph_ptr with a "state-player" property
      instead, this way we will be able to modify the automata I/O routines
      to support games directly.
      
      * spot/misc/game.cc, spot/misc/game.hh: Rewrite the solver and
      pg_printer interface.
      * bin/ltlsynt.cc: Adjust.
      * NEWS: Mention this change.
      * doc/org/concepts.org: Mention the state-player property.
      25c75c55
  12. 07 Sep, 2020 4 commits
  13. 03 Sep, 2020 2 commits
  14. 02 Sep, 2020 2 commits
  15. 01 Sep, 2020 2 commits
  16. 05 Aug, 2020 1 commit
    • Alexandre Duret-Lutz's avatar
      [buddy] get rid of many recursive algorithms · 6f76121b
      Alexandre Duret-Lutz authored
      This patch addresses the BuDDy part of #396,
      reported by Florian Renkin and Reed Oei.
      
      * src/kernel.c, src/kernel.h: Declare a bddrecstack and
      associated macros.  Resize it when new variable are declared.
      * src/cache.h: Add a BddCache_index macro.
      * src/bddop.c (not_rec, apply_rec, quant_rec, appquant_rec,
      support_rec, ite_rec, compose_rec, restrict_rec, satone_rec,
      satoneset_rec): Rewrite using this stack to get rid of the recursion.
      6f76121b
  17. 03 Aug, 2020 2 commits