1. 03 Apr, 2018 1 commit
  2. 02 Apr, 2018 1 commit
  3. 30 Mar, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      sat_minimize: improve logs and document Python bindings · c766f58d
      Alexandre Duret-Lutz authored
      * spot/priv/satcommon.cc, spot/priv/satcommon.hh: Make it possible to
      set the log file without setting the environment variable.  Adjust
      print_log to take the input state and print it as a new column.
      * spot/twaalgos/dtbasat.cc, spot/twaalgos/dtwasat.cc: Adjust all
      calls to print_log.  Fix log output for incremental approaches.
      Prefer purge_unreachable_states() over stats_reachable().  Do
      not call scc_filter() on colored automata.
      * spot/twaalgos/dtwasat.hh: Document the new "log" option.
      * NEWS: Mention the changes.
      * tests/python/satmin.ipynb: New file.
      * tests/Makefile.am: Add it.
      * doc/org/satmin.org, doc/org/tut.org: Link to it.
      * doc/org/satmin.org, bin/man/spot-x.x: Adjust description
      of CSV files.
      * bench/dtgbasat/gen.py, bench/dtgbasat/tabl.pl,
      bench/dtgbasat/tabl1.pl, bench/dtgbasat/tabl2.pl,
      bench/dtgbasat/tabl3.pl, bench/dtgbasat/tabl4.pl: Adjust for
      the new column.
      * spot/misc/satsolver.cc, spot/misc/satsolver.hh (stats): Make it
      const.
      * python/spot/__init__.py (sat_minimize): Add display_log and
      return_log options.
      * tests/python/ipnbdoctest.py: Adjust to not compare SAT-minimization
      logs as they contain timings.
      c766f58d
  4. 28 Mar, 2018 4 commits
    • Alexandre Duret-Lutz's avatar
      specialized translation for GF(guarantee) and FG(safety) · 7a65bdf6
      Alexandre Duret-Lutz authored
      This is adapted from a proposition in a paper by J. Esparza,
      J. Křentínský, and S. Sickert, submitted to LICS'18.  We should add
      proper references to the code and documentation once that paper is
      accepted.
      
      * spot/twaalgos/gfguarantee.cc, spot/twaalgos/gfguarantee.hh:
      New files.
      * spot/twaalgos/Makefile.am, python/spot/impl.i: Add them.
      * spot/twa/fwd.hh: Add a forward declaration of bdd_dict_ptr.
      * spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh: Make it
      possible to call finalize() from the translator subclass.  Constify
      all the do_* functions while we are there.
      * spot/twaalgos/translate.cc, spot/twaalgos/translate.hh: Add
      a "gf-guarantee" option to decide whether to use the new translation.
      * bin/spot-x.cc: Document it.
      * tests/core/dca2.test, tests/core/genltl.test,
      tests/core/ltl2tgba2.test, tests/core/parity2.test,
      tests/core/satmin.test, tests/python/automata.ipynb,
      tests/python/sbacc.py: Adjust test cases.
      * tests/python/except.py: Add a couple more tests.
      7a65bdf6
    • Alexandre Duret-Lutz's avatar
      autfilt: fix --sat-minimize -B · 82796c04
      Alexandre Duret-Lutz authored
      Fixes #340.
      
      * bin/common_post.cc: -B implies -S.
      * tests/core/satmin2.test: Test this.
      82796c04
    • Alexandre Duret-Lutz's avatar
      python: fix error message of translate()/posprocess() · ee30f966
      Alexandre Duret-Lutz authored
      * python/spot/__init__.py: Here.
      * NEWS: Mention the bug.
      ee30f966
    • Alexandre Duret-Lutz's avatar
      to_dca/to_nca: fix handling of co-Büchi input · 7957a231
      Alexandre Duret-Lutz authored
      * spot/twaalgos/cobuchi.cc (to_dca, to_nca): Do not process
      the input if it is already co-Büchi.
      * tests/core/dca.test: Test this.
      * NEWS: Mention the bug.
      7957a231
  5. 25 Mar, 2018 2 commits
  6. 23 Mar, 2018 2 commits
  7. 19 Mar, 2018 1 commit
  8. 18 Mar, 2018 3 commits
  9. 16 Mar, 2018 3 commits
  10. 15 Mar, 2018 1 commit
  11. 14 Mar, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      acc: strengthen is_generalized_rabin() and is_generalized_streett() · b6e44e6b
      Alexandre Duret-Lutz authored
      * spot/twa/acc.cc: These functions were segfaulting on acceptance
      conditions such as "Acceptance: 3 t" or "Acceptance: 3 f".
      The issue was revealed on branch "next" by the change that print_dot()
      display the acceptance condition by default, but we want the fix on
      master as well.
      * NEWS: Mention the issue.
      b6e44e6b
  12. 10 Mar, 2018 2 commits
    • Alexandre Duret-Lutz's avatar
      dot: make "a" the default · 2a308182
      Alexandre Duret-Lutz authored
      Fixes #319.
      
      * spot/twaalgos/dot.cc: Enable "a" by default.
      * bin/common_aoutput.cc, NEWS: Document it.
      * doc/org/autfilt.org, doc/org/concepts.org, doc/org/dstar2tgba.org,
      doc/org/hierarchy.org, doc/org/ltl2tgba.org, doc/org/oaut.org,
      doc/org/randaut.org, doc/org/satmin.org, doc/org/tut23.org,
      doc/org/tut24.org, doc/org/tut30.org, doc/org/tut31.org: Adjust or
      simplify the documentation.
      * tests/core/det.test, tests/core/dstar.test, tests/core/monitor.test,
      tests/core/neverclaimread.test, tests/core/readsave.test,
      tests/core/tgbagraph.test, tests/core/wdba.test,
      tests/python/_autparserr.ipynb, tests/python/automata-io.ipynb,
      tests/python/automata.ipynb, tests/python/highlighting.ipynb
      tests/python/ltsmin-dve.ipynb, tests/python/ltsmin-pml.ipynb,
      tests/python/product.ipynb, tests/python/testingaut.ipynb,
      tests/python/word.ipynb: Adjust test cases.
      2a308182
    • Alexandre Duret-Lutz's avatar
      acc: strengthen is_generalized_rabin() and is_generalized_streett() · 15fdac60
      Alexandre Duret-Lutz authored
      * spot/twa/acc.cc: These functions were segfaulting on acceptance
      conditions such as "Acceptance: 3 t" or "Acceptance: 3 f".
      The issue was revealed on branch "next" by the change that print_dot()
      display the acceptance condition by default, but we want the fix on
      master as well.
      * NEWS: Mention the issue.
      15fdac60
  13. 23 Feb, 2018 1 commit
  14. 21 Feb, 2018 1 commit
    • Maximilien Colange's avatar
      Improve cleanup_parity · e945beb6
      Maximilien Colange authored
      * spot/twaalgos/parity.cc: cleanup_parity and cleanup_parity_here are
        now better at finding useless parity colors
      * tests/python/parity.py: test it
      * NEWS: document the change
      e945beb6
  15. 20 Feb, 2018 2 commits
  16. 19 Feb, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      fix handling of Rabin-like input for dnf_to_dca() · 81e5357e
      Alexandre Duret-Lutz authored
      The bug is mentioned by Maximilien Colange in a comment to issue #317,
      but turned out to be unrelated to that original issue.
      
      * spot/twaalgos/totgba.cc (dnf_to_streett): Save the correspondence
      between the created states an the DNF clause in a named property.
      * doc/org/concepts.org, spot/twaalgos/totgba.hh: Mention the new
      property.
      * spot/twaalgos/cobuchi.cc (save_inf_nca_st): Rewrite using the named
      property.  Relying on seen marks and trying to deduce the matching
      original clause could only work from plain Rabin.
      * tests/core/dca.test: Add the test from Maximilien.
      * NEWS: Mention the issue.
      81e5357e
  17. 17 Feb, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      fix tra_to_tba() · e42fea09
      Alexandre Duret-Lutz authored
      Fixes #324, reported by Tobias Meggendorfer and František Blahoudek.
      
      * spot/twa/acc.hh (rs_pairs_view::paired_with): Rename as...
      (rs_pairs_view::paired_with_fin):... this and adjust the code.
      * spot/twaalgos/remfin.cc: Use paired_with_fin instead of
      paired_with, and do it once per pair.
      * tests/core/remfin.test: Add a test case.
      * NEWS: Mention the issue.
      e42fea09
  18. 16 Feb, 2018 1 commit
  19. 24 Jan, 2018 1 commit
    • Maximilien Colange's avatar
      Improve IAR construction · 1ebd86de
      Maximilien Colange authored
      spot::iar() was fixed to handle correctly Rabin-like conditions.
      It also now supports Streett-like conditions.
      
      * NEWS, spot/twaalgos/postproc.cc: document it
      * spot/twaalgos/rabin2parity.cc, spot/twaalgos/rabin2parity.hh:
        implement it
      * tests/core/rabin2parity.test, tests/python/except.py: test it
      1ebd86de
  20. 23 Jan, 2018 1 commit
  21. 20 Jan, 2018 2 commits
  22. 19 Jan, 2018 1 commit
  23. 16 Jan, 2018 2 commits
    • Maximilien Colange's avatar
      Rabin to parity translation · 7e02aae3
      Maximilien Colange authored
      * spot/twaalgos/rabin2parity.cc, spot/twaalgos/rabin2parity.hh:
        implement it
      * spot/twaalgos/postproc.cc: use it
      * spot/twaalgos/Makefile.am: build the new files
      * NEWS: document the new function
      * python/spot/impl.i: Python bindings for the new function
      * tests/Makefile.am, tests/core/rabin2parity.test: test the new function
      7e02aae3
    • Maximilien Colange's avatar
      Typos and duplicates · 7bf68b4c
      Maximilien Colange authored
      * spot/twaalgos/degen.cc: typo in an error message
      * NEWS: fix typos and remove duplicates
      7bf68b4c
  24. 14 Jan, 2018 3 commits
    • Alexandre Duret-Lutz's avatar
      work around issue #317 · c920825f
      Alexandre Duret-Lutz authored
      * spot/twaalgos/cobuchi.cc: Call sbacc() on transition-based input.
      * tests/Makefile.am: Remove XFAIL_TESTS.
      * NEWS: Adjust.
      c920825f
    • Alexandre Duret-Lutz's avatar
      postproc: add support for co-Büchi output · 61b0a542
      Alexandre Duret-Lutz authored
      * spot/twaalgos/cobuchi.cc, spot/twaalgos/cobuchi.hh (to_nca): New
      function.
      (weak_to_cobuchi): New internal function, used in to_nca and to_dca
      when appropriate.
      * spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh: Implement
      the CoBuchi option.
      * python/spot/__init__.py: Support it in Python.
      * bin/common_post.cc: Add support for --buchi.
      * bin/autfilt.cc: Remove the --dca option.
      * tests/core/dca.test, tests/python/automata.ipynb: Adjust and add
      more tests.  In particular, add more complex persistence and
      recurrence formulas to the list of dca.test.
      * tests/python/dca.test: Adjust and rename to...
      * tests/core/dca2.test: ... this.  Add more tests, to the point
      that this is now failing, as described in issue #317.
      * tests/python/dca.py: Remove.
      * tests/Makefile.am: Adjust.
      61b0a542
    • Alexandre Duret-Lutz's avatar
      fix streett_to_generalized_buchi · 9464043d
      Alexandre Duret-Lutz authored
      Fixes #316.
      
      * spot/twaalgos/totgba.cc: Fix confusing definition of scc_inf_wo_fin.
      * tests/python/streett_totgba2.py: New test case.
      * tests/Makefile.am: Add it.
      * NEWS: Mention the bug.
      9464043d
  25. 10 Jan, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      misc: fix some down_cast issues · 8a74ae6c
      Alexandre Duret-Lutz authored
      We had new failure on MinGW with GCC believing that some pointer
      returned by down_cast could be NULL; and the down_cast function was in
      the global namespace.
      
      * spot/misc/casts.hh: Rewrite.
      * NEWS: Mention the small issues.
      * tests/core/ikwiad.cc, tests/core/ngraph.cc: Adjust to use
      spot::down_cast instead of down_cast.
      8a74ae6c