1. 30 Apr, 2020 2 commits
  2. 29 Apr, 2020 1 commit
    • 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
  3. 20 Apr, 2020 1 commit
  4. 12 Apr, 2020 1 commit
  5. 11 Apr, 2020 2 commits
    • Alexandre Duret-Lutz's avatar
      relabel_bse: fix incorrect detection of common APs · 33289f51
      Alexandre Duret-Lutz authored
      Based on a report by Jean Kreber.
      
      * spot/tl/relabel.cc (cut_points): Really connect children of Boolean
      operators using undirected edges, not directed ones.
      * tests/core/ltlrel.test: Add test cases.
      * NEWS: Mention the bug.
      33289f51
    • Alexandre Duret-Lutz's avatar
      ignore false edges in emptiness checks and scc_info · 0b258202
      Alexandre Duret-Lutz authored
      Based on reports by Florian Renkin and Jens Kreber.
      
      * spot/twaalgos/bfssteps.cc, spot/twaalgos/couvreurnew.cc,
      spot/twaalgos/gtec/gtec.cc, spot/twaalgos/gv04.cc,
      spot/twaalgos/magic.cc, spot/twaalgos/sccinfo.cc
      spot/twaalgos/se05.cc, spot/twaalgos/tau03.cc: Ignore bddfalse edges.
      * spot/twaalgos/gtec/gtec.hh: Remove debugging function.
      * tests/core/neverclaimread.test: Adjust.
      * tests/python/ecfalse.py: New test file.
      * tests/Makefile.am: Add it.
      * NEWS: Mention the bug.
      0b258202
  6. 10 Apr, 2020 1 commit
  7. 05 Apr, 2020 2 commits
  8. 30 Mar, 2020 1 commit
  9. 26 Mar, 2020 1 commit
  10. 13 Mar, 2020 3 commits
  11. 12 Mar, 2020 4 commits
  12. 11 Mar, 2020 3 commits
  13. 09 Mar, 2020 1 commit
    • Alexandre Duret-Lutz's avatar
      ltlcross: do not use remove_fin anymore · 4e99518d
      Alexandre Duret-Lutz authored
      * bin/ltlcross.cc: Since is_empty() now works with arbitrary
      acceptance conditions, calling remove_fin() is not necessary anymore.
      * tests/core/ltlcrossce.test: Adjust.
      * NEWS: Mention the change.
      4e99518d
  14. 08 Mar, 2020 2 commits
  15. 24 Feb, 2020 1 commit
    • Florian Renkin's avatar
      CAR: new algorithm for paritizing · 96531f29
      Florian Renkin authored
      * NEWS: Mention it.
      * spot/twaalgos/car.cc, spot/twaalgos/car.hh, tests/python/car.py:
      New files.
      * spot/twaalgos/Makefile.am, tests/Makefile.am: Add them.
      * python/spot/impl.i: Include CAR.
      * spot/twa/acc.cc, spot/twa/acc.hh, spot/twa/twagraph.cc,
      spot/twa/twagraph.hh: Add supporting methods.
      96531f29
  16. 19 Feb, 2020 6 commits
  17. 15 Feb, 2020 2 commits
  18. 10 Feb, 2020 2 commits
  19. 05 Feb, 2020 1 commit
  20. 03 Feb, 2020 3 commits
    • Alexandre Duret-Lutz's avatar
      fix degeneralize_tba after accepting transition · b733d486
      Alexandre Duret-Lutz authored
      * spot/twaalgos/degen.cc (degeneralize_tba): Here.
      * tests/python/pdegen.py, tests/python/simstate.py: Adjust expected
      values.
      * NEWS: Mention the bug.
      b733d486
    • Alexandre Duret-Lutz's avatar
      partial_degeneralize: a support for disjunction of Fin · f9e75de6
      Alexandre Duret-Lutz authored
      * spot/twaalgos/degen.cc, spot/twaalgos/degen.hh: Implement this.
      Also throw a runtime error in case were todegen does not match any
      subformula.
      * tests/python/pdegen.py: Add tests.
      f9e75de6
    • Alexandre Duret-Lutz's avatar
      improve partial_degeneralize() on several cases · f1008c15
      Alexandre Duret-Lutz authored
      On these 4 cases, added to pdegen.py, and supplied by Florian Renkin,
      partial_degeneralize() is now at least as good as degeneralize_tba(),
      and sometimes better.  This is achieved as follows: (1) a
      propagate_marks procedure is introduced to propagate marks as far as
      possible on the automaton (e.g., common outgoing marks can be push
      onto the incoming transitions and vice-versa), (2) the
      degeneralization order is compute dynamically, and (3) whenever and
      fully-accepting transition is taken in the original automaton, the
      destination level is chosen to be the highest existing level.
      
      * spot/twaalgos/degen.cc,
      spot/twaalgos/degen.hh (propagate_marks_vector, propagate_marks_here):
      New functions.
      (partial_degeneralize): Improve, as described above.
      * tests/python/pdegen.py: Add test cases.
      f1008c15