1. 29 Jun, 2021 1 commit
  2. 12 May, 2021 4 commits
  3. 11 May, 2021 1 commit
  4. 29 Mar, 2021 1 commit
    • Jérôme Dubois's avatar
      simulation: Add simulation based reduction · fb066ada
      Jérôme Dubois authored
      * spot/twaalgos/simulation.hh, spot/twaalgos/simulation.cc: Add
        reduce_direct_sim(), reduce_direct_cosim() and
        reduce_direct_iterated() wich reduce an automaton using simulation.
        This functions wrap the class direct_sim wich compute simulation
        with a new method.
      * doc/spot.bib: Add ref.
      * tests/python/simstate.py: Add tests for the new simulation.
      fb066ada
  5. 03 Mar, 2021 1 commit
  6. 18 Jan, 2021 4 commits
  7. 07 Jan, 2021 1 commit
  8. 05 Jan, 2021 1 commit
  9. 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
  10. 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
  11. 19 Nov, 2020 1 commit
  12. 08 Nov, 2020 5 commits
  13. 07 Oct, 2020 1 commit
  14. 06 Oct, 2020 1 commit
    • Alexandre Duret-Lutz's avatar
      postprocess, translate: add support for Büchi (not state-based) · 9cc1bdf1
      Alexandre Duret-Lutz authored
      spot/twaalgos/postproc.hh: Introduce options Buchi and
      GeneralizedBuchi.  The latter is similar to TGBA but the former differs
      from BA in that it does not imply state-based acceptance, since that
      can be specified separately.  Also all other acceptance types are not
      abbreviated, so those new names make more sense.
      * NEWS: Mention that.
      * spot/twaalgos/postproc.cc, spot/twaalgos/translate.cc: Adjust
      to support Buchi and GeneralizedBuchi without breaking BA and TGBA.
      * bin/autfilt.cc, bin/common_aoutput.cc, bin/common_post.cc,
      bin/ltl2tgta.cc, doc/org/tut10.org, doc/org/tut12.org,
      doc/org/tut30.org, python/spot/__init__.py,
      tests/python/automata.ipynb, tests/python/langmap.py,
      tests/python/misc-ec.py, tests/python/satmin.ipynb,
      tests/python/satmin.py, tests/python/toweak.py: Use the new names.
      * tests/Makefile.am: Add missing langmap.py.
      9cc1bdf1
  15. 28 Sep, 2020 1 commit
  16. 24 Sep, 2020 1 commit
  17. 23 Sep, 2020 1 commit
  18. 22 Sep, 2020 1 commit
    • Philipp Schlehuber's avatar
      game: reimplement parity game solving · 133896d5
      Philipp Schlehuber authored
      * spot/misc/game.cc, spot/misc/game.hh: More efficient implementation
      of Zielonka's algorithm to solve parity games.  Now supports SCC
      decomposition and efficient handling of certain special cases.
      * doc/org/concepts.org: Document "strategy" and "state-winner"
      properties.
      * bin/ltlsynt.cc, tests/python/paritygame.ipynb: Adjust.
      * tests/core/ltlsynt.test: Add more tests.
      133896d5
  19. 10 Sep, 2020 2 commits
  20. 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
  21. 08 Sep, 2020 3 commits
    • 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
  22. 07 Sep, 2020 3 commits
  23. 03 Aug, 2020 3 commits