1. 30 Jul, 2019 2 commits
  2. 17 Jul, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      forbid the use of std::endl on std::cerr · 09c93a3a
      Alexandre Duret-Lutz authored
      std::cerr will flush after each operator<< by default, so it's simpler
      to use \n instead of std::endl, especially if we can merge \n into the
      previous string.  Ideally we should prefer \n for std::cout as well,
      but there are reasonable cases where we want to call std::endl there,
      so it's hard to enforce.
      
      * tests/sanity/style.test: Diagnose occurrences of cerr.*<<.*endl.
      * bin/autcross.cc, bin/autfilt.cc, bin/ltlcross.cc, bin/ltlsynt.cc,
      spot/tl/formula.cc, spot/twa/bdddict.cc, tests/core/checkpsl.cc,
      tests/core/checkta.cc, tests/core/consterm.cc, tests/core/emptchk.cc,
      tests/core/equalsf.cc, tests/core/ikwiad.cc, tests/core/kind.cc,
      tests/core/length.cc, tests/core/ltlrel.cc, tests/core/parity.cc,
      tests/core/randtgba.cc, tests/core/reduc.cc, tests/core/syntimpl.cc,
      tests/ltsmin/modelcheck.cc: Fix them.
      09c93a3a
  3. 12 Jul, 2019 2 commits
  4. 11 Jul, 2019 1 commit
  5. 09 Jul, 2019 3 commits
    • Alexandre Duret-Lutz's avatar
      product: fix handling of output_aborter · 1d7ad07c
      Alexandre Duret-Lutz authored
      * spot/twaalgos/product.cc: The res pointer should be
      passed by reference since we reset it to nullptr when
      output_aborter says "too large".
      * python/spot/impl.i: Add binding for powerset.hh,
      so we can use output_aborter in Python.
      * tests/python/prodexpt.py: Test it.
      1d7ad07c
    • Alexandre Duret-Lutz's avatar
      genem: cite our ATVA'19 paper · 5af4612e
      Alexandre Duret-Lutz authored
      * doc/spot.bib (baier.19.atva): New reference.
      * spot/twaalgos/genem.hh: Cite it.
      5af4612e
    • Alexandre Duret-Lutz's avatar
      tl: eight new simplification rules · 0d9cc29b
      Alexandre Duret-Lutz authored
      * NEWS, doc/tl/tl.tex: Document the rules.
      * spot/tl/simplify.cc: Implement them.
      * tests/core/reduccmp.test: Test them.
      * tests/core/det.test, tests/core/ltl2tgba2.test,
      tests/python/stutter-inv.ipynb, tests/core/385.test: Adjust.
      0d9cc29b
  6. 05 Jul, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      deprecate spot::acc_cond::format() · bfe0ada6
      Alexandre Duret-Lutz authored
      * NEWS: Mention it.
      * spot/twa/acc.hh (spot::acc_cond::format): Deprecate.
      (spot::acc_cond::mark_t::as_string): New function.
      * spot/taalgos/dot.cc: Use mark_t::as_string().
      * spot/priv/satcommon.cc, spot/priv/satcommon.hh,
      spot/twaalgos/dtwasat.cc, spot/twaalgos/emptiness.cc,
      tests/core/acc.cc, tests/core/acc.test: Adjust to use << directly.
      bfe0ada6
  7. 30 Jun, 2019 1 commit
  8. 22 Jun, 2019 2 commits
  9. 21 Jun, 2019 2 commits
  10. 20 Jun, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      simulation: improve merging of transiant-SCCs · f3e57901
      Alexandre Duret-Lutz authored
      * spot/twaalgos/simulation.cc: Code this.
      * tests/core/det.test, tests/core/dra2dba.test,
      tests/core/satmin.test, tests/core/sim3.test,
      tests/python/decompose.ipynb, tests/python/dualize.py: Adjust test
      cases.
      * NEWS: Mention the optimization.
      f3e57901
  11. 18 Jun, 2019 4 commits
    • Alexandre Duret-Lutz's avatar
      toparity: revert symmetry-based optimization of LAR · c66b3d88
      Alexandre Duret-Lutz authored
      Fixes #390.
      
      * spot/twaalgos/toparity.cc: Revert the relevant part of 516e9536.
      * tests/python/toparity.py: Add test case.
      * NEWS: Mention the issue.
      c66b3d88
    • Alexandre Duret-Lutz's avatar
      toparity: typo in pretty print · a8e47d0b
      Alexandre Duret-Lutz authored
      * spot/twaalgos/toparity.cc: Fix pretty print.
      a8e47d0b
    • Alexandre Duret-Lutz's avatar
      gfguarantee: fix #357 again · 8df5f513
      Alexandre Duret-Lutz authored
      The previous patch triggered this issue again, failing
      core/ltl2tgba2.test.
      
      * spot/twaalgos/gfguarantee.cc: Separate the replaying of history from
      the modification of the automaton.
      * NEWS: Mention the bug.
      * tests/python/twagraph-internals.ipynb, tests/python/automata.ipynb:
      Adjust.
      8df5f513
    • Alexandre Duret-Lutz's avatar
      simplify: GF(f)=GF(dnf(f)) FG(f)=FG(cnf(f)) · da5d23f0
      Alexandre Duret-Lutz authored
      These rules come from Delag's paper, and help some cases
      in issue #385.
      
      * spot/tl/simplify.cc: Implement the simplification.
      * doc/tl/tl.tex, NEWS: Document it.
      * tests/core/385.test: New file.
      * tests/Makefile.am: Add it.
      * tests/core/reduccmp.test: More tests.
      * tests/core/ltl2tgba2.test: Adjust one improved case.
      * tests/python/automata.ipynb, tests/python/twagraph-internals.ipynb:
      Adjust expected output, as the cnf/dnf reorder some subformulas.
      da5d23f0
  12. 14 Jun, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      use a bibtex file to collect all references in Doxygen · df326e03
      Alexandre Duret-Lutz authored
      * doc/tl/tl.bib: Move ...
      * doc/spot.bib: ... here, and augment it with all references that
      appeared verbatim in Doxygen comments.
      * doc/Makefile.am, doc/tl/Makefile.am
      doc/tl/tl.tex: Adjust for the move.
      * doc/Doxyfile.in: Point to spot.bib.
      * spot/gen/automata.hh, spot/gen/formulas.hh, spot/misc/game.hh,
      spot/misc/minato.hh spot/taalgos/emptinessta.hh,
      spot/taalgos/minimize.hh, spot/taalgos/tgba2ta.hh, spot/tl/formula.hh,
      spot/tl/remove_x.hh, spot/tl/simplify.hh, spot/tl/snf.hh,
      spot/twaalgos/cobuchi.hh, spot/twaalgos/cycles.hh,
      spot/twaalgos/dualize.hh, spot/twaalgos/gtec/gtec.hh,
      spot/twaalgos/gv04.hh, spot/twaalgos/ltl2taa.hh,
      spot/twaalgos/ltl2tgba_fm.hh, spot/twaalgos/magic.hh,
      spot/twaalgos/minimize.hh, spot/twaalgos/parity.hh,
      spot/twaalgos/powerset.hh, spot/twaalgos/randomgraph.hh,
      spot/twaalgos/se05.hh, spot/twaalgos/simulation.hh,
      spot/twaalgos/strength.hh, spot/twaalgos/stutter.hh,
      spot/twaalgos/tau03.hh, spot/twaalgos/totgba.hh,
      spot/twaalgos/toweak.hh: Use \cite instead of a verbatim bibtex entry.
      df326e03
  13. 13 Jun, 2019 1 commit
  14. 12 Jun, 2019 3 commits
  15. 11 Jun, 2019 1 commit
  16. 07 Jun, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      genaut: introduce --m-nba · cba01232
      Alexandre Duret-Lutz authored
      * bin/genaut.cc: Implement the --m-nba option.
      * spot/gen/automata.hh, spot/gen/automata.cc: Add the generation code.
      * NEWS, bin/man/genaut.x: Document it.
      * doc/org/genaut.org: Update.
      * tests/core/genaut.test, tests/core/parity2.test: Add some tests.
      cba01232
  17. 04 Jun, 2019 3 commits
  18. 02 Jun, 2019 2 commits
  19. 28 May, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      introduce output_aborter, and use it in ltlcross · a8504509
      Alexandre Duret-Lutz authored
      * spot/twaalgos/alternation.cc, spot/twaalgos/alternation.hh,
      spot/twaalgos/complement.cc, spot/twaalgos/complement.hh,
      spot/twaalgos/determinize.cc, spot/twaalgos/determinize.hh,
      spot/twaalgos/minimize.cc, spot/twaalgos/minimize.hh,
      spot/twaalgos/postproc.cc, spot/twaalgos/postproc.hh,
      spot/twaalgos/powerset.cc, spot/twaalgos/powerset.hh,
      spot/twaalgos/product.cc, spot/twaalgos/product.hh: Use an
      output_aborter argument to abort if the output is too large.
      * bin/ltlcross.cc: Use complement() with an output_aborter
      so that ltlcross will not attempt to build complement larger
      than 500 states or 5000 edges.  Add --determinize-max-states
      and --determinize-max-edges options.
      * tests/core/ltlcross3.test, tests/core/ltlcrossce2.test,
      tests/core/sccsimpl.test, tests/core/wdba2.test,
      tests/python/stutter-inv.ipynb: Adjust test cases.
      * NEWS: Document this.
      * bin/spot-x.cc: Add documentation for postprocessor's
      det-max-states and det-max-edges arguments.
      * doc/org/ltlcross.org: Update description.
      a8504509
  20. 24 May, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      word: introduce use_all_aps() · 36d20696
      Alexandre Duret-Lutz authored
      This allows fixing issue #388 reported by Victor Khomenko.
      
      * spot/twaalgos/word.cc, spot/twaalgos/word.hh (use_all_aps): New
      method.
      * tests/python/stutter-inv.ipynb: Use it.
      * tests/python/stutter.py: New file, with Victor's test case.
      * tests/Makefile.am: Add python/stutter.py.
      36d20696
  21. 20 May, 2019 1 commit
    • Alexandre Duret-Lutz's avatar
      tl: fix handling of f##[0:0]g, and of ##[0:n]g · 90a88d0b
      Alexandre Duret-Lutz authored
      The first issue was reported by Victor Khomenko.
      
      * spot/tl/formula.cc: Introduce a single-argument
      version of sugar_delay().
      * spot/parsetl/parsetl.yy: Use it.
      * doc/tl/tl.tex, spot/tl/formula.hh: Adjust doc.
      * tests/core/ltlfilt.test, tests/core/sugar.test: More tests.
      90a88d0b
  22. 19 May, 2019 1 commit
  23. 18 May, 2019 4 commits