1. 26 Oct, 2022 1 commit
  2. 19 Oct, 2022 1 commit
  3. 17 Oct, 2022 1 commit
    • Alexandre Duret-Lutz's avatar
      reduce_parity: add layered option · b0c299b9
      Alexandre Duret-Lutz authored
      * spot/twaalgos/parity.cc: Implement it.
      * spot/twaalgos/parity.hh, NEWS: Document it.
      * tests/python/parity.ipynb: Demonstrate it.  This is the only test so
      far, but more uses are coming.
      b0c299b9
  4. 13 Oct, 2022 2 commits
  5. 10 Oct, 2022 2 commits
  6. 08 Oct, 2022 2 commits
  7. 05 Oct, 2022 1 commit
    • Alexandre Duret-Lutz's avatar
      translate, postproc: improve parity output · 344e01d4
      Alexandre Duret-Lutz authored
      * spot/twaalgos/translate.cc: When producing Parity output, split LTL
      as we do in the Generic case.
      * spot/twaalgos/postproc.hh, spot/twaalgos/postproc.cc: Use
      acd_transform() and add an "acd" option to disable this.
      * bin/spot-x.cc, NEWS: Document this.
      * tests/core/genltl.test, tests/core/minusx.test,
      tests/core/parity2.test: Adjust test cases for improved outputs.
      344e01d4
  8. 04 Oct, 2022 1 commit
  9. 23 Sep, 2022 4 commits
    • Alexandre Duret-Lutz's avatar
      update gitlab references · 51caa558
      Alexandre Duret-Lutz authored
      As LRDE is being renamed LRE, gitlab is one of the first URL to
      migrate.  The old URL is still supported, but we want to only use the
      new one eventually.
      
      * .dir-locals.el, .gitlab-ci.yml, HACKING, NEWS, doc/org/concepts.org,
      doc/org/install.org, doc/org/setup.org, elisp/Makefile.am,
      elisp/hoa-mode.el, tests/ltsmin/README: Update to the new gitlab URL.
      51caa558
    • Alexandre Duret-Lutz's avatar
      translate: add a branch-post option · 3729dfad
      Alexandre Duret-Lutz authored
      * spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Here.
      * NEWS, bin/spot-x.cc: Mention it.
      * tests/core/genltl.test: Test it.
      3729dfad
    • Alexandre Duret-Lutz's avatar
      genltl: introduce --eil-gsi · 7ed62f7e
      Alexandre Duret-Lutz authored
      Based on a mail from Edmond Irani Liu.  The test case also serves for
      the previous patch.
      
      * bin/genltl.cc, spot/gen/formulas.cc, spot/gen/formulas.hh: Add it.
      * NEWS: Mention it.
      * tests/core/genltl.test: Test it.
      7ed62f7e
    • Alexandre Duret-Lutz's avatar
      introduce delay_branching_here · 3efab05c
      Alexandre Duret-Lutz authored
      This is motivated by an example sent by Edmond Irani Liu,
      that will be tested in next patch.
      
      * spot/twaalgos/dbranch.cc, spot/twaalgos/dbranch.hh: New files.
      * python/spot/impl.i, spot/twaalgos/Makefile.am: Add them.
      * spot/twaalgos/translate.cc: Call delay_branching_here
      unconditionally.
      * spot/twa/twagraph.cc (defrag_states): Do not assume
      that games are alternating.
      * tests/core/genltl.test: Adjust expected numbers.
      * tests/python/dbranch.py: New file.
      * tests/Makefile.am: Add it.
      3efab05c
  10. 14 Sep, 2022 1 commit
    • Alexandre Duret-Lutz's avatar
      ltlsynt: add options --dot and --hide-status · c1c874b1
      Alexandre Duret-Lutz authored
      * bin/ltlsynt.cc: Implement these options.
      * bin/common_aoutput.hh, bin/common_aoutput.cc (automaton_format_opt):
      Make extern.
      * NEWS: Mention the new options.
      * doc/org/ltlsynt.org: Use dot output in documentation.
      * tests/core/ltlsynt.test: Quick test of the new options.
      c1c874b1
  11. 13 Sep, 2022 1 commit
    • Alexandre Duret-Lutz's avatar
      postproc: introduce -x merge-states-min · b3b22388
      Alexandre Duret-Lutz authored
      * spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh: Introduce a
      merge-states-min option.
      * bin/spot-x.cc: Document it.
      * spot/gen/automata.cc, spot/gen/automata.hh, bin/genaut.cc: Add
      option to generate cyclist test cases.
      * NEWS: Document the above.
      * tests/core/included.test: Add test cases that used to be too slow.
      b3b22388
  12. 12 Sep, 2022 1 commit
    • Alexandre Duret-Lutz's avatar
      degen: learn to work on generalized-Co-Büchi as well · bdac5351
      Alexandre Duret-Lutz authored
      * spot/twaalgos/degen.hh, spot/twaalgos/degen.cc: Adjust
      degeneralize() and degeneralize_tba() to work on generalized-co-Büchi.
      * NEWS: Mention this.
      * spot/twaalgos/cobuchi.hh, spot/twaalgos/cobuchi.cc (to_nca): Use
      degeneralization on generalized-co-Büchi.
      * spot/twaalgos/postproc.cc: Use degeneralization for generalized
      co-Büchi as well.
      * bin/autfilt.cc: Improve chain products of co-Büchi automata by using
      generalization if too many colors are needed.
      * tests/core/prodchain.test, tests/python/pdegen.py: Add test cases.
      bdac5351
  13. 06 Sep, 2022 1 commit
  14. 14 Aug, 2022 1 commit
    • Alexandre Duret-Lutz's avatar
      do not use a global variable to define the number of available threads · d1b84955
      Alexandre Duret-Lutz authored
      * python/spot/impl.i: Make parallel_policy implicitly contractible.
      * spot/graph/graph.hh (sort_edges_srcfirst_): Pass a parallel_policy
      explicitly.
      * spot/twa/twagraph.hh, spot/twa/twagraph.cc (merge_states): Likewise.
      * spot/misc/common.cc: Remove file.
      * spot/misc/common.hh (set_nthreads, get_nthreads): Remove, and
      replace with...
      (parallel_policy): ... this.
      * spot/misc/Makefile.am, tests/python/mergedge.py, NEWS: Adjust.
      d1b84955
  15. 23 Jul, 2022 1 commit
    • Alexandre Duret-Lutz's avatar
      rename pg_print() as print_pg() and add it to to_str() · 8b93b696
      Alexandre Duret-Lutz authored
      * NEWS: Mention those change.
      * spot/twaalgos/game.hh (print_pg): New function.
      (pg_print): Mark as deprecated.
      * spot/twaalgos/game.cc (pg_print): Redirect to print_pg().
      (print_pg): Update to output state names.
      * python/spot/__init__.py: Teach to_str() about print_pg().
      * bin/ltlsynt.cc: Adjust to call print_pg().
      * tests/python/games.ipynb: Add an example.
      * tests/core/ltlsynt.test: Adjust to remove the "INIT" note.
      8b93b696
  16. 22 Jul, 2022 1 commit
    • Alexandre Duret-Lutz's avatar
      parseaut: Add support for PGSolver's format · 444e2b5b
      Alexandre Duret-Lutz authored
      * spot/parseaut/parseaut.yy, spot/parseaut/scanaut.ll: Add rules for
      PGSolver's format.
      * spot/parseaut/public.hh: PGAME is a new type of output.
      * tests/core/pgsolver.test: New file.
      * tests/Makefile.am: Add it.
      * tests/python/games.ipynb: More exemples.
      * NEWS: Mention the new feature.
      444e2b5b
  17. 23 Jun, 2022 3 commits
  18. 22 Jun, 2022 2 commits
    • Alexandre Duret-Lutz's avatar
      contains: generalize second argument to a twa · 288b1c79
      Alexandre Duret-Lutz authored
      This was triggered by a question from Pierre Ganty on the mailing
      list.
      
      * spot/twaalgos/contains.hh, spot/twaalgos/contains.cc (contains):
      Generalize second argument to const_twa_ptr instead of
      const_twa_graph_ptr.
      * NEWS: Mention this.
      * tests/python/ltsmin-pml.ipynb: Show that it work.
      * THANKS: Mention Pierre.
      288b1c79
    • Alexandre Duret-Lutz's avatar
      ltlsynt: add --from-pgame option to read parity games · be28365d
      Alexandre Duret-Lutz authored
      * bin/common_file.cc, bin/common_file.hh (output_file): Add a
      force_append option.
      * bin/ltlsynt.cc: Implement the --from-pgame option, and
      fix suppot for --csv when multiple inputs are processed.
      * NEWS: Mention the new option.
      * tests/core/syfco.test: Add a test case.
      * tests/core/ltlsynt-pgame.test: New file.
      * tests/Makefile.am: Add it.
      be28365d
  19. 21 Jun, 2022 1 commit
    • Alexandre Duret-Lutz's avatar
      Add a --enable-pthread option to activate experimental threading code · 23908f3d
      Alexandre Duret-Lutz authored
      * NEWS, README, doc/org/compile.org: Mention the option and
      its effect on compilation requirements.
      * configure.ac: Add the --enable-pthread option, and ENABLE_PTHREAD
      macro.
      * doc/org/g++wrap.in, spot/Makefile.am, spot/libspot.pc.in: Compile
      with -pthread conditionally.
      * spot/graph/graph.hh, spot/twa/twagraph.cc: Adjust the code to not
      use thread-local variables, and let the pthread code be optional.
      * .gitlab-ci.yml: Activate --enable-pthread in two configurations.
      23908f3d
  20. 24 May, 2022 1 commit
  21. 20 May, 2022 2 commits
    • Alexandre Duret-Lutz's avatar
      zlktree: use a cache in the construction of zielonka_tree · b1120844
      Alexandre Duret-Lutz authored
      This largely speeds up the computation for conditions
      like "Rabin n" sharing a lot of subtrees.
      
      Also implement options to stop the construction if the shape is wrong.
      
      * spot/twaalgos/zlktree.cc, spot/twaalgos/zlktree.hh: Implement the
      cache and the options.
      * tests/python/zlktree.ipynb, tests/python/zlktree.py: New tests.
      b1120844
    • Alexandre Duret-Lutz's avatar
      complete: do not force Büchi on universal automata · f784e405
      Alexandre Duret-Lutz authored
      * spot/twaalgos/complete.hh: Adjust documentation.
      * spot/twaalgos/complete.cc: If the acceptance condition is a
      tautology, delay the forcing of Büchi acceptance until we are sure it
      is needed.
      * NEWS: Mention the change.
      f784e405
  22. 18 May, 2022 5 commits
  23. 17 May, 2022 2 commits
  24. 09 May, 2022 1 commit
    • Alexandre Duret-Lutz's avatar
      twagraph: improve copy of kripke_graph · 013c879b
      Alexandre Duret-Lutz authored
      Fix #505, Reported by Edmond Irani Liu.
      
      * spot/twa/twagraph.cc (copy): Deal with kripke_graph in a better way.
      * spot/twaalgos/hoa.cc: Do not force the use of named-states since
      when the input is a kripke_graph.
      * tests/python/kripke.py: Adjust test cases.
      * NEWS: Mention the change.
      * THANKS: Add Edmund.
      013c879b
  25. 03 May, 2022 1 commit