1. 17 Oct, 2020 1 commit
  2. 09 Oct, 2020 1 commit
  3. 07 Oct, 2020 1 commit
  4. 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
  5. 28 Sep, 2020 1 commit
  6. 24 Sep, 2020 4 commits
    • Philipp Schlehuber's avatar
      Improving split and reorganizing · 29055c81
      Philipp Schlehuber authored
      * spot/twaalgos/synthesis.cc, spot/twaalgos/synthesis.hh: New files
      regrouping the functionnalities split and apply_strategy for synthesis
      * python/spot/impl.i, spot/twaalgos/Makefile.am: Add them.
      * spot/twaalgos/split.cc, spot/twaalgos/split.hh: No longer contains
      the splits necessary for for synthesis, moved to
      spot/twaalgos/synthesis.cc, spot/twaalgos/split.hh Split is now faster
      and reduces the number of intermediate states, reducing the overall
      size of the arena
      * spot/misc/game.cc, spot/misc/game.hh: Renaming propagate_players to
      alternate_players.
      * tests/core/ltlsynt.test, tests/python/split.py: Update tests.
      * bin/ltlsynt.cc: Adjust to new split. Swap order of split and
      to_parity for lar.
      29055c81
    • Alexandre Duret-Lutz's avatar
      game: mention Oink · ca043bd6
      Alexandre Duret-Lutz authored
      * doc/spot.bib (vandijk.18.tacas): New entry.
      * spot/misc/game.hh (solve_parity_game): Mention it.
      ca043bd6
    • Alexandre Duret-Lutz's avatar
      game: let highlight_strategy work for non-parity games · 324b0872
      Alexandre Duret-Lutz authored
      This is required by an upcoming patch by Jérôme, solving reachability
      games.
      
      * spot/misc/game.cc (highlight_strategy): Do not require parity
      acceptance.
      324b0872
    • Alexandre Duret-Lutz's avatar
      game: fix handling of useless SCCs · 392c1a0e
      Alexandre Duret-Lutz authored
      This is a bug I introduced while merging Philipp's patch.
      
      * spot/misc/game.cc (parity_game::solve): Set the strategy for player
      0 in useless SCCs.
      (parity_game::fix_scc): Do not use sub_game_ to detect edges exiting
      the SCC.
      * tests/python/game.py: New file.
      * tests/Makefile.am: Add it.
      392c1a0e
  7. 23 Sep, 2020 7 commits
  8. 22 Sep, 2020 2 commits
  9. 19 Sep, 2020 2 commits
    • Alexandre Duret-Lutz's avatar
      * AUTHORS: Add Philipp. · ea3e3964
      Alexandre Duret-Lutz authored
      ea3e3964
    • Philipp Schlehuber's avatar
      game: reimplement print_aiger · 0d43beda
      Philipp Schlehuber authored
      * spot/twaalgos/aiger.cc, spot/twaalgos/aiger.hh: Reimplement
      print_aiger for speed gain, also heuristics to minimize the number
      of gates as well as different encoding types have been added.
      * bin/ltlsynt.cc: Make the new options for print-aiger available.
      * tests/core/ltlsynt.test: Adjust tests.
      0d43beda
  10. 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
  11. 17 Sep, 2020 1 commit
  12. 16 Sep, 2020 5 commits
  13. 13 Sep, 2020 1 commit
  14. 12 Sep, 2020 1 commit
  15. 10 Sep, 2020 2 commits
  16. 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
  17. 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
  18. 07 Sep, 2020 4 commits