1. 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
  2. 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
  3. 09 Jan, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      genltl: add --gf-implies · 0b71df3f
      Alexandre Duret-Lutz authored
      * spot/gen/formulas.cc, spot/gen/formulas.hh: Implement
      LTL_GF_IMPLIES.
      * bin/genltl.cc: Add --gf-implies.
      * NEWS: Mention it.
      * tests/core/genltl.test: Use it.
      0b71df3f
  4. 08 Jan, 2018 2 commits
    • Alexandre Duret-Lutz's avatar
      python: add colored parity support to postproc and translate · f369db6c
      Alexandre Duret-Lutz authored
      * python/spot/impl.i: Bind is_colored().
      * python/spot/__init__.py: Add Colored support to postproc.
      * tests/python/parity.py: Add a test case.
      f369db6c
    • Alexandre Duret-Lutz's avatar
      postproc: add support for colored-parity · bd6dc7a8
      Alexandre Duret-Lutz authored
      * spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh: Add support
      for a colored option.
      * bin/common_post.cc, bin/common_post.hh bin/autfilt.cc,
      bin/ltl2tgba.cc, bin/dstar2tgba.cc: Add support for --colored-parity.
      * bin/ltldo.cc: Adjust as well for consistency, even if --parity and
      --colored-parity is not used here.
      * tests/core/parity2.test: Add tests.
      * doc/org/autfilt.org, doc/org/ltl2tgba.org: Add examples.
      * NEWS: Mention --colored-parity.
      bd6dc7a8
  5. 07 Jan, 2018 2 commits
    • Alexandre Duret-Lutz's avatar
      python: remove error recovery checks from the public notebooks · 6bad8aeb
      Alexandre Duret-Lutz authored
      * tests/python/_autparserr.ipynb: New files, containing error
      checking code from automata-io.ipynb and piperead.ipynb.
      * tests/python/automata-io.ipynb: Remove error checks, and pipe
      examples from piperead.ipynb.
      * tests/python/piperead.ipynb: Delete.
      * tests/python/word.ipynb: Move error checking code...
      * tests/python/_word.ipynb: ... in this new file.
      * doc/org/tut.org, tests/Makefile.am: Adjust.
      6bad8aeb
    • Alexandre Duret-Lutz's avatar
      python: upgrade notebook format to v4 · 58e64e75
      Alexandre Duret-Lutz authored
      Fixes #311.
      
      * tests/python/ipnbdoctest.py: Adjust to process the new format,
      with a lot of inspiration from Vcsn's copy of this file.
      * tests/python/_altscc.ipynb, tests/python/_aux.ipynb,
      tests/python/acc_cond.ipynb, tests/python/accparse.ipynb,
      tests/python/alternation.ipynb, tests/python/atva16-fig2a.ipynb,
      tests/python/atva16-fig2b.ipynb, tests/python/automata-io.ipynb,
      tests/python/automata.ipynb, tests/python/decompose.ipynb,
      tests/python/formulas.ipynb, tests/python/gen.ipynb,
      tests/python/highlighting.ipynb, tests/python/ltsmin-dve.ipynb,
      tests/python/ltsmin-pml.ipynb, tests/python/parity.ipynb,
      tests/python/piperead.ipynb, tests/python/product.ipynb,
      tests/python/randaut.ipynb, tests/python/randltl.ipynb,
      tests/python/stutter-inv.ipynb, tests/python/testingaut.ipynb,
      tests/python/word.ipynb: Upgrade to the new format.
      * NEWS: Mention the change.
      58e64e75
  6. 06 Jan, 2018 3 commits
    • Alexandre Duret-Lutz's avatar
      ltlcross: detect remove_fin failures · 020c9811
      Alexandre Duret-Lutz authored
      Fixes #314, reported by František Blahoudek.
      
      * bin/ltlcross.cc: Here.
      * tests/core/ltlcross3.test: Add new test case.
      * NEWS: Mention the bug.
      020c9811
    • Alexandre Duret-Lutz's avatar
      remove_fin: use simplify_acceptance · a924bc56
      Alexandre Duret-Lutz authored
      * spot/twaalgos/remfin.cc: Simplify acceptance before trying the
      different strategies.
      * spot/twaalgos/cleanacc.cc: Skip simplify_complementary_marks_here()
      on generalized Büchi.
      * tests/core/remfin.test, tests/python/tra2tba.py: Adjust.
      * spot/twaalgos/totgba.cc: Simplify the result of Streett->GBA.
      * NEWS: Adjust.
      a924bc56
    • Alexandre Duret-Lutz's avatar
      simplify_acceptance: fix handling of first edge · 2feba6ad
      Alexandre Duret-Lutz authored
      Fixes #315.
      
      * spot/twaalgos/cleanacc.cc (simplify_acceptance_here): Do not
      compare the first edge against previous_a.
      * tests/core/accsimpl.test: New file.
      * tests/Makefile.am: Add it.
      * NEWS: Mention the bug.
      2feba6ad
  7. 04 Jan, 2018 1 commit
  8. 02 Jan, 2018 3 commits
  9. 25 Dec, 2017 3 commits
  10. 24 Dec, 2017 1 commit
  11. 23 Dec, 2017 1 commit
  12. 22 Dec, 2017 5 commits
  13. 19 Dec, 2017 2 commits
  14. 18 Dec, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      introduce check_determinism() · ac80b07d
      Alexandre Duret-Lutz authored
      * spot/twaalgos/isdet.hh, spot/twaalgos/isdet.cc (check_determinism):
      New function.
      * NEWS: Mention it.
      * tests/python/semidet.py: New file.
      * tests/Makefile.am: Add it.
      ac80b07d
  15. 10 Dec, 2017 1 commit
    • Alexandre Duret-Lutz's avatar
      Add support for computing operator nesting depth · 62d1e021
      Alexandre Duret-Lutz authored
      * spot/tl/hierarchy.hh, spot/tl/hierarchy.cc (nesting_depth): New
      function.
      * python/spot/__init__.py: Also make it a method of formula in Python
      * bin/common_output.cc, bin/common_output.hh: Implement
      --stats=%[OP]n.
      * NEWS: Mention it.
      * tests/core/format.test, tests/python/formulas.ipynb: Test it.
      62d1e021
  16. 28 Nov, 2017 2 commits
  17. 24 Nov, 2017 4 commits
    • Alexandre Duret-Lutz's avatar
      tests: reduce the memory/time footprint of ltl2dstar.test · d219e4a5
      Alexandre Duret-Lutz authored
      * tests/core/ltl2dstar.test: Reduce the amount of tests performed on
      one formula that is problematic for ltl2dstar.
      d219e4a5
    • Alexandre Duret-Lutz's avatar
      tests: git rid of all the tool=tool assignents · a9a375cc
      Alexandre Duret-Lutz authored
      Our use of
        ltl2tgba=ltl2tgba
        autfilt=autfilt
        ...
      all over the test cases comes from the time where those tools were not
      in PATH and we actually had something like
        ltl2tgba=../../bin/ltl2tgba
        autfilt=../../bin/autfilt
      
      But today that is useless, and we prefer to write ltl2tgba rather than
      $ltl2tgba, so let's remove this old cruft.
      
      * tests/core/basimul.test, tests/core/det.test, tests/core/lbt.test,
      tests/core/lenient.test, tests/core/ltl2dstar.test,
      tests/core/ltl2dstar2.test, tests/core/ltl2dstar3.test,
      tests/core/ltl2dstar4.test, tests/core/ltlcross2.test,
      tests/core/ltlcross3.test, tests/core/ltlcross4.test,
      tests/core/ltlcrossce2.test, tests/core/ltldo.test,
      tests/core/ltlfilt.test, tests/core/optba.test,
      tests/core/prodor.test, tests/core/rand.test,
      tests/core/randomize.test, tests/core/remfin.test,
      tests/core/satmin.test, tests/core/sbacc.test,
      tests/core/strength.test, tests/core/stutter-ltl.test,
      tests/core/stutter-tgba.test, tests/core/unabbrevwm.test,
      tests/core/unambig.test: Get rid of all tool=tool assignments.
      a9a375cc
    • Maximilien Colange's avatar
      Fix ltlsynt tests · ce3eeb44
      Maximilien Colange authored
      * tests/core/ltlsynt.test: Escape newlines and test PGsolver printer
      ce3eeb44
    • Maximilien Colange's avatar
      Fix script running IPython tests · d358521b
      Maximilien Colange authored
      * tests/python/ipnbdoctest.py: skip test when jupyter is not found
      d358521b
  18. 23 Nov, 2017 3 commits
    • Maximilien Colange's avatar
      Improve ltlsynt interface · 1da0afba
      Maximilien Colange authored
      To ease debugging and testing, ltlsynt can output the synthesized
      strategy as an automaton, not just an aiger circuit.
      Also, its exit code has been changed to something meaningful.
      
      * bin/ltlsynt.cc: Various improvements: options, exit code, code style
      * spot/twaalgos/aiger.hh, spot/twaalgos/aiger.cc,
        spot/twaalgos/Makefile.am: Move the aiger printer to separate files
      * tests/core/ltlsynt.test: Clean up and update test file
      * tests/Makefile.am: Add the test file to the test suite
      * NEWS: document the new aiger printer
      * doc/org/concepts.org: document the named property "synthesis-outputs",
        used by print_aiger
      1da0afba
    • Alexandre Duret-Lutz's avatar
    • Alexandre Duret-Lutz's avatar
      introduce formula::is_leaf() · 974a4238
      Alexandre Duret-Lutz authored
      Fixes #307.
      
      * spot/tl/formula.hh: Here.
      * tests/python/ltlparse.py: Test it.
      * NEWS: Mention it.
      974a4238
  19. 22 Nov, 2017 1 commit