1. 28 Sep, 2020 1 commit
  2. 24 Sep, 2020 4 commits
    • Philipp Schlehuber's avatar
      Improving split and reorganizing · 29055c81
      Philipp Schlehuber authored and Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz committed
      * 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
  3. 23 Sep, 2020 7 commits
  4. 22 Sep, 2020 2 commits
  5. 19 Sep, 2020 2 commits
  6. 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
  7. 17 Sep, 2020 1 commit
  8. 16 Sep, 2020 5 commits
  9. 13 Sep, 2020 1 commit
  10. 12 Sep, 2020 1 commit
  11. 10 Sep, 2020 2 commits
  12. 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
  13. 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
  14. 07 Sep, 2020 4 commits
  15. 03 Sep, 2020 2 commits
  16. 02 Sep, 2020 2 commits