1. 18 May, 2020 28 commits
  2. 16 May, 2020 3 commits
    • Alexandre Duret-Lutz's avatar
      ltlsynt: make sure the previous Xor optimization actually works · 66aa6d08
      Alexandre Duret-Lutz authored
      * spot/tl/simplify.hh, spot/tl/simplify.cc,
      spot/twaalgos/translate.cc: Update the tl_simplification
      options after all preferences have been given.
      * bin/ltlsynt.cc: Display the size of the translation output.
      * tests/core/ltlsynt.test: Add test case.
      66aa6d08
    • Alexandre Duret-Lutz's avatar
      translate: improve handling of Xor and Equiv at top-level for -G -D · 6bfa9793
      Alexandre Duret-Lutz authored
      * spot/tl/formula.hh: Add variant of formula::is that support 4
      arguments.
      * spot/tl/simplify.hh, spot/tl/simplify.cc: Add option keep_top_xor
      to preserve Xor and Equiv at the top-level.
      * spot/twaalgos/translate.cc: Adjust ltl-split to deal with Xor and
      Equiv for the -D -G case.
      * NEWS: Mention that.
      * tests/core/ltl2tgba2.test: Add test case.
      * tests/python/simstate.py: Adjust expected result.
      6bfa9793
    • Alexandre Duret-Lutz's avatar
      product: add product_xor() and product_xnor() · 3ab2dd17
      Alexandre Duret-Lutz authored
      * spot/twaalgos/product.cc, spot/twaalgos/product.hh: Add those
      functions.
      * tests/python/_product_weak.ipynb, tests/python/except.py: Test them.
      * NEWS: Mention them.
      3ab2dd17
  3. 30 Apr, 2020 5 commits
  4. 29 Apr, 2020 2 commits
    • Alexandre Duret-Lutz's avatar
      dot: fix #393 · a7051b32
      Alexandre Duret-Lutz authored
      * spot/twaalgos/dot.cc: Add support for option 'E', and default to
      rectangle nodes for large labels.
      * bin/common_aoutput.cc, NEWS: Document it.
      * tests/core/alternating.test, tests/core/dstar.test,
      tests/core/readsave.test, tests/core/sccdot.test,
      tests/core/tgbagraph.test, tests/python/_product_weak.ipynb,
      tests/python/alternation.ipynb, tests/python/atva16-fig2b.ipynb,
      tests/python/automata.ipynb, tests/python/decompose.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/pdegen.py,
      tests/python/satmin.ipynb, tests/python/stutter-inv.ipynb: Adjust all
      test cases.
      a7051b32
    • Alexandre Duret-Lutz's avatar
      dot: fix #392 · 3ea63e9a
      Alexandre Duret-Lutz authored
      * spot/twaalgos/dot.cc: Add tooltips to "..." states and edges.
      * tests/core/readsave.test: Test this.
      * tests/python/highlighting.ipynb: Adjust.
      3ea63e9a
  5. 25 Apr, 2020 2 commits
    • Alexandre Duret-Lutz's avatar
      postproc: fix issue #402 · 67060420
      Alexandre Duret-Lutz authored
      * spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh,
      spot/twaalgos/translate.cc: Introduce a gen-reduce-parity option and
      use it on sub-automata built by ltl-split.
      * bin/spot-x.cc: Document it.
      * tests/core/ltl2tgba2.test: Add test case reported by Juraj Major.
      67060420
    • Alexandre Duret-Lutz's avatar
      ltlsynt: fix lar.old implementation · fe340ae8
      Alexandre Duret-Lutz authored
      * bin/ltlsynt.cc: Make sure to_parity_old() receive a deterministic
      automaton, for correctness.   Also call reduce_parity() afterward,
      to match what was done in 2.8.7.
      * tests/core/ltlsynt.test: Include lar.old in the comparison of all
      results to make sure it give the same result as the other 3
      algorithms.
      fe340ae8